Module `E_ACSL.Bound_variables`

val get_preprocessed_quantifier : 
  Frama_c_kernel.Cil_types.predicate ->
  ((Frama_c_kernel.Cil_types.term
    * Frama_c_kernel.Cil_types.logic_var
    * Frama_c_kernel.Cil_types.term)
     list
   * Frama_c_kernel.Cil_types.predicate)
    Error.result

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

val add_guard_for_small_type : 
  Frama_c_kernel.Cil_types.logic_var ->
  Frama_c_kernel.Cil_types.predicate ->
  unit

Adds an optional additional guard condition that comes from the typing

val get_guard_for_small_type : 
  Frama_c_kernel.Cil_types.logic_var ->
  Frama_c_kernel.Cil_types.predicate option

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

val replace : 
  Frama_c_kernel.Cil_types.predicate ->
  (Frama_c_kernel.Cil_types.term
   * Frama_c_kernel.Cil_types.logic_var
   * Frama_c_kernel.Cil_types.term)
    list ->
  Frama_c_kernel.Cil_types.predicate ->
  unit

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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `E_ACSL.Bound_variables`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module E_ACSL.Bound_variables

Module `E_ACSL.Bound_variables`