Module Logic_normalizer

module Logic_normalizer: sig .. end

This module is dedicated to some preprocessing on the predicates:


val preprocess : Cil_types.file -> unit

Preprocess all the predicates of the ast and store the results

val preprocess_annot : Cil_types.code_annotation -> unit

Preprocess of the predicate of a single code annotation and store the results

val preprocess_predicate : Cil_types.predicate -> unit

Preprocess a predicate and its children and store the results

val get_pred : Cil_types.predicate -> Cil_types.predicate

Retrieve the preprocessed form of a predicate

val get_term : Cil_types.term -> Cil_types.term

Retrieve the preprocessed form of a term

val clear : unit -> unit

clear the table of normalized predicates