E_ACSL.Logic_normalizer
This module is dedicated to some preprocessing on the predicates:
Pvalid
and Pvalid_read
clauses with an adequate Pinitialized
clause;Papp
by a corresponding term obtained as an application Tapp
The predicates that have undergone these changed are called the preprocessed predicates.val preprocess : Frama_c_kernel.Cil_types.file -> unit
Preprocess all the predicates of the ast and store the results
val preprocess_annot : Frama_c_kernel.Cil_types.code_annotation -> unit
Preprocess of the predicate of a single code annotation and store the results
val preprocess_predicate : Frama_c_kernel.Cil_types.predicate -> unit
Preprocess a predicate and its children and store the results
val get_pred :
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.predicate
Retrieve the preprocessed form of a predicate
val get_term : Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.term
Retrieve the preprocessed form of a term