Module `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.t list Error.result

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Labels/index.html

Module `E_ACSL.Labels`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Labels/index.html

Module E_ACSL.Labels

Module `E_ACSL.Labels`