Frama-C API - simplifier
method copy : simplifier
method assume : F.pred -> unit
Assumes the hypothesis
method target : F.pred -> unit
Give the predicate that will be simplified later
method infer : F.pred list
Add new hypotheses implied by the original hypothesis.
Currently simplify an expression. It must returns a equivalent formula from the assumed hypotheses.
Currently simplify an hypothesis before assuming it. It must return a weaker formula from the assumed hypotheses.
Currently simplify a branch condition. It must return an equivalent formula from the assumed hypotheses.