E_ACSL.Logic_normalizerThis 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 -> unitPreprocess all the predicates of the ast and store the results
val preprocess_annot : Frama_c_kernel.Cil_types.code_annotation -> unitPreprocess of the predicate of a single code annotation and store the results
val preprocess_predicate : Frama_c_kernel.Cil_types.predicate -> unitPreprocess a predicate and its children and store the results
val get_pred :
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.predicateRetrieve the preprocessed form of a predicate
val get_term : Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.termRetrieve the preprocessed form of a term