module Eval_non_linear: sig
.. end
Evaluation of non-linear expressions.
val eval_expr_with_deps_state : with_alarms:CilE.warn_mode ->
Locations.Zone.t option ->
Cvalue.Model.t ->
Cil_types.exp ->
Cvalue.Model.t * Locations.Zone.t option * Locations.Location_Bytes.t
Same functionality as
Eval_exprs.eval_expr_with_deps_state
. For
expressions in which some l-values appear multiple times, proceed
by disjunction on their abstract value, in order to gain precision.
val compute_non_linear : Cil_types.exp -> (Cil_types.lval * Locations.location option) list