diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index 9a535134ce61730528cc9ed81d7eb2c3fe3c5af9..0adbbd5ebd2178991f430073708a86c7c5f6503d 100644 --- a/src/plugins/eva/Eva.mli +++ b/src/plugins/eva/Eva.mli @@ -685,6 +685,18 @@ module Logic_inout: sig result: Cil_types.varinfo option -> Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t + (** Zones of an lvalue term of an assigns clause. *) + type tlval_zones = { + under: Locations.Zone.t; (** Under-approximation of the memory zone. *) + over: Locations.Zone.t; (** Over-approximation of the memory zone. *) + deps: Locations.Zone.t; (** Dependencies needed to evaluate the address. *) + } + + (** Evaluation of the memory zones and dependencies of an lvalue term from an + assigns clause, in the given cvalue state for a read or write access. *) + val assigns_tlval_to_zones: + Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option + (** Evaluate the assigns clauses of the given function in its given pre-state, and compare them with the given froms (computed by the from plugin). Emits warnings if needed, and sets statuses to the assigns clauses. *) diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml index 344e7cd9f1a3e3992df5b7fd571a8cbd5f0ce4a9..ce12bb0f25478cd2cd9a23dbb6344017e4d4679c 100644 --- a/src/plugins/eva/legacy/eval_terms.ml +++ b/src/plugins/eva/legacy/eval_terms.ml @@ -2773,6 +2773,9 @@ let eval_tlval_as_zone ~alarm_mode access env t = in over +let tlval_deps env t = (eval_term_as_lval ~alarm_mode:Ignore env t).ldeps + + let () = (* TODO: deprecate loc_to_loc, move loc_to_locs into Value *) Db.Properties.Interp.loc_to_loc := diff --git a/src/plugins/eva/legacy/eval_terms.mli b/src/plugins/eva/legacy/eval_terms.mli index a8b326ffc3dbb4651441e06591a75a501a4b3130..ff51402c4982af6c308f8e68c4a12a71f48cd19f 100644 --- a/src/plugins/eva/legacy/eval_terms.mli +++ b/src/plugins/eva/legacy/eval_terms.mli @@ -116,5 +116,11 @@ val eval_predicate : Returns None on either an evaluation error or on unsupported construct. *) val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option +(** [tlval_deps env t] computes the logic dependencies needed to evaluate the + address of lvalue term [t] in the given evaluation environment [env]. + @raises LogicEvalError on evaluation errors, unsupported constructs, or + if [t] is not an lvalue term. *) +val tlval_deps: eval_env -> Cil_types.term -> logic_deps + val reduce_by_predicate : eval_env -> bool -> predicate -> eval_env diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml index a505839980c5e4433fe373fec607fa6fab6682bf..e4b4c543a701109dc90c688a4f202ce58c430887 100644 --- a/src/plugins/eva/legacy/logic_inout.ml +++ b/src/plugins/eva/legacy/logic_inout.ml @@ -100,6 +100,24 @@ let assigns_outputs_to_zone ~result state assigns = | WritesAny -> Locations.Zone.top | Writes l -> List.fold_left treat_asgn Locations.Zone.bottom l +type tlval_zones = { + under: Locations.Zone.t; + over: Locations.Zone.t; + deps: Locations.Zone.t; +} + +let assigns_tlval_to_zones state access tlval = + let env = Eval_terms.env_post_f ~pre:state ~post:state ~result:None () in + let alarm_mode = Eval_terms.Ignore in + try + let under, over = + Eval_terms.eval_tlval_as_zone_under_over ~alarm_mode access env tlval + in + let deps = join_logic_deps (Eval_terms.tlval_deps env tlval) in + Some { under; over; deps; } + with Eval_terms.LogicEvalError _ -> None + + (* -------------------------------------------------------------------------- *) (* --- Verify assigns clauses --- *) (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli index 92d6afd81687589a37b2bfbdcadea6bfe67a6cba..7e478d9b4c5cada150d08b830a78cdd701c3e283 100644 --- a/src/plugins/eva/legacy/logic_inout.mli +++ b/src/plugins/eva/legacy/logic_inout.mli @@ -50,6 +50,18 @@ val assigns_outputs_to_zone: result: Cil_types.varinfo option -> Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t +(** Zones of an lvalue term of an assigns clause. *) +type tlval_zones = { + under: Locations.Zone.t; (** Under-approximation of the memory zone. *) + over: Locations.Zone.t; (** Over-approximation of the memory zone. *) + deps: Locations.Zone.t; (** Dependencies needed to evaluate the address. *) +} + +(** Evaluation of the memory zones and dependencies of an lvalue term from an + assigns clause, in the given cvalue state for a read or write access. *) +val assigns_tlval_to_zones: + Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option + (** Evaluate the assigns clauses of the given function in its given pre-state, and compare them with the given froms (computed by the from plugin). Emits warnings if needed, and sets statuses to the assigns clauses. *)