module Labels:sig
..end
Pre-analysis for Labeled terms and predicates.
This pre-analysis records, for each labeled term or predicate, the place where the translation must happen.
The list of labeled terms or predicates to be translated for a given
statement is provided by Labels.at_for_stmt
.
Pre-analysis for Labeled terms and predicates.
val get_first_inner_stmt : Cil_types.stmt -> Cil_types.stmt
If the given statement has a label, return the first statement of the block. Otherwise return the given statement.
val at_for_stmt : Cil_types.stmt -> Analyses_datatype.At_data.Set.t Error.result
Not_memoized
if the labels pre-analysis was not run.val preprocess : Cil_types.file -> unit
Analyse sources to find the statements where a labeled predicate or term should be translated.
val reset : unit -> unit
Reset the results of the pre-anlaysis.
val _debug : unit -> unit
Print internal state of labels translation.
val has_empty_quantif_ref : ((Cil_types.term * Cil_types.logic_var * Cil_types.term) list -> bool)
Stdlib.ref