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 -> Trace.t -> Trace.t   val add_statement : Cil_types.stmt -> Trace.t -> Trace.t   val set_compute_trace : bool -> unit end