sig
type t
val pretty : Format.formatter -> Trace.t -> unit
val bottom : Trace.t
val top : Trace.t
val join : Trace.t -> Trace.t -> Trace.t
val narrow : Trace.t -> Trace.t -> Trace.t
val initial : Cil_types.kernel_function -> Trace.t
val add_disjunction :
Property.t -> Cil_types.predicate Cil_types.named -> Trace.t -> Trace.t
val add_statement : Cil_types.stmt -> Trace.t -> Trace.t
val set_compute_trace : bool -> unit
end