Module Logic_simplification

module Logic_simplification: sig .. end
Basic simplification over Promelaast.typed_condition

Given a list of terms (representing a conjunction), if a positive call or return is present, then all negative ones are obvious and removed


val tand : Promelaast.typed_condition ->
Promelaast.typed_condition -> Promelaast.typed_condition

smart constructors for typed conditions


val tor : Promelaast.typed_condition ->
Promelaast.typed_condition -> Promelaast.typed_condition
val tnot : Promelaast.typed_condition -> Promelaast.typed_condition

simplifications


val simplifyCond : Promelaast.typed_condition ->
Promelaast.typed_condition * Promelaast.typed_condition list list
Given a condition, this function does some logical simplifications and returns an equivalent DNF form together with the simplified version

Given a condition, this function does some logical simplifications. It returns both the simplified condition and a disjunction of conjunctions of parametrized call or return.

val simplifyTrans : Promelaast.typed_condition Promelaast.trans list ->
Promelaast.typed_condition Promelaast.trans list *
Promelaast.typed_condition list list list
Given a transition list, this function returns the same transition list with simplifyCond done on each cross condition. Uncrossable transition are removed.

Given a list of transitions, this function returns the same list of transition with simplifyCond done on its cross condition

val dnfToCond : Promelaast.typed_condition list list -> Promelaast.typed_condition
Given a DNF condition, it returns a condition in Promelaast.condition form. WARNING : empty lists not supported
val simplifyDNFwrtCtx : Promelaast.typed_condition list list ->
Cil_types.kernel_function ->
Promelaast.funcStatus -> Promelaast.typed_condition
Given a DNF condition, it returns the same condition simplified according to the context (function name and status). Hence, the returned condition is without any Call/Return stmts.