Module Subdivided_evaluation

module Subdivided_evaluation: sig .. end

Subdivision of the evaluation on non-linear expressions: for expressions in which some l-values appear multiple times, proceed by disjunction on their abstract value, in order to gain precision.


module type Forward_Evaluation = sig .. end
module Make: 
functor (Value : Abstract_value.External-> 
functor (Loc : Abstract_location.S with type value = Value.t-> 
functor (Valuation : Eval.Valuation with type value = Value.t and type loc = Loc.location-> 
functor (Eva : Forward_Evaluation with type value := Value.t and type valuation := Valuation.t-> sig .. end