E_ACSL.Labels
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
.
val get_first_inner_stmt :
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.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 :
Frama_c_kernel.Cil_types.stmt ->
Analyses_datatype.At_data.Set.t Error.result
val preprocess : Frama_c_kernel.Cil_types.file -> unit
Analyse sources to find the statements where a labeled predicate or term should be translated.
val has_empty_quantif_ref :
((Frama_c_kernel.Cil_types.term
* Frama_c_kernel.Cil_types.logic_var
* Frama_c_kernel.Cil_types.term)
list ->
bool)
Stdlib.ref