Module Logic_simplification

module Logic_simplification: sig .. end

Basic simplification over Promelaast.typed_condition


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.