module Trace: sig
.. end
Traces.
type
t
Type of traces.
val pretty : Format.formatter -> t -> unit
val bottom : t
No trace. Should be used only as a base case for a no-op join.
val top : t
Unknown trace. Should be used only to forget a trace.
val join : t -> t -> t
val narrow : t -> t -> t
val initial : Cil_types.kernel_function -> t
Create a trace, or add an element at the end of a trace.
val add_disjunction : Property.t -> Cil_types.predicate -> t -> t
val add_statement : Cil_types.stmt -> t -> t
val set_compute_trace : bool -> unit
Set to false to set all traces to top.