Frama-C:
Plug-ins:
Libraries:

Frama-C API - Bound_variables

  • returns

    the preprocessed of a quantified predicate the (term * logic_var * term) list is the list of all the quantified variables along with their syntactic guards, and the predicate is the goal: the original predicate with all the quantifiers removed.

  • raises Typing_error

    if predicate cannot be typed.

  • raises Abort.fatal

    if predicate has not been preprocessed.

Adds an optional additional guard condition that comes from the typing

  • returns

    the optional additional guard for a quantified logic variables. It may happen that the syntactic guard of the variable can be refined with the type of the variable, this additional predicate translates this refinement

Replace the computed guards. This is because the typing sometimes simplifies the computed bounds, so we allow for storing new bounds

val clear_guards : unit -> unit

Clear the table of guard conditions for quantified variables

val preprocess : Frama_c_kernel.Cil_types.file -> unit

Preprocess all the quantified predicates in the ast and store the result in an hashtable

val preprocess_annot : Frama_c_kernel.Cil_types.code_annotation -> unit

Preprocess the quantified predicate in a given code annotation

val preprocess_predicate : Frama_c_kernel.Cil_types.predicate -> unit

Preprocess the quantified predicate in a given predicate