Module Labels

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
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