module Bound_variables:sig..end
Module for preprocessing the quantified predicates. Predicates with
quantifiers are hard to translate, so we delegate some of the work to
a preprocessing phase. At the end of this phase, all the quantified
predicates should have an associated preprocessed form vars * goal where
vars is a list of guarded variables in the right ordergoal is the predicate under the quantifications
The guarded variables in the list vars are of
type term * logic_var * term * predicate option, where a tuple
(t1,v,t2,p) indicates that v is a logic variable with the two
guards t1 <= x < t2 and p is an additional optional guard to
intersect the first guard with the provided type for the variable vval get_preprocessed_quantifier : Cil_types.predicate ->
((Cil_types.term * Cil_types.logic_var * Cil_types.term) list *
Cil_types.predicate)
Error.resultGetters and setters
(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 removedval add_guard_for_small_type : Cil_types.logic_var -> Cil_types.predicate -> unitAdds an optional additional guard condition that comes from the typing
val get_guard_for_small_type : Cil_types.logic_var -> Cil_types.predicate optionval replace : Cil_types.predicate ->
(Cil_types.term * Cil_types.logic_var * Cil_types.term) list ->
Cil_types.predicate -> unitReplace the computed guards. This is because the typing sometimes simplifies the computed bounds, so we allow for storing new bounds
val clear_guards : unit -> unitClear the table of guard conditions for quantified variables
val preprocess : Cil_types.file -> unitPreprocess all the quantified predicates in the ast and store the result in an hashtable
val preprocess_annot : Cil_types.code_annotation -> unitPreprocess the quantified predicate in a given code annotation
val preprocess_predicate : Cil_types.predicate -> unitPreprocess the quantified predicate in a given predicate