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
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
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 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