Frama-C API - 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.

If the given statement has a label, return the first statement of the block. Otherwise return the given statement.

  • returns

    the set of labeled predicates and terms to be translated on the given statement.

  • raises Not_memoized

    if the labels pre-analysis was not run.

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 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 : ((Frama_c_kernel.Cil_types.term * Frama_c_kernel.Cil_types.logic_var * Frama_c_kernel.Cil_types.term) list -> bool) Stdlib.ref