Frama-C API - Subdivided_evaluation
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 ... endmodule Make (Value : Abstract.Value.External) (Loc : Abstract_location.S with type value = Value.t) (Valuation : Eval.Valuation with type value = Value.t and type loc = Loc.location) (Eva : Forward_Evaluation with type value := Value.t and type valuation := Valuation.t) : sig ... end