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
module Logic_infos : sig ... endThe analyses in Logic_normalizer may:
val get_pred :
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.predicateRetrieve the preprocessed form of a predicate
val get_orig_pred :
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.predicateRetrieve the original form of the given predicate
val get_term : Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.termRetrieve the preprocessed form of a term
val get_orig_term :
Frama_c_kernel.Cil_types.term ->
Frama_c_kernel.Cil_types.termRetrieve the original form of the given term