diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 1d48b8bd770c42905f1018e69de78a5447f7e547..dfe0c43c7dfc87df17a5c15b403739a53f44baa7 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -610,6 +610,22 @@ end
module Logic_inout: sig
+ (** Returns the list of behaviors of the given function that are active for
+ the given initial state. *)
+ val valid_behaviors:
+ Cil_types.kernel_function -> Cvalue.Model.t -> Cil_types.behavior list
+
+ (** Evaluation of the memory zone read by the \from part of an assigns clause,
+ in the given cvalue state. *)
+ val assigns_inputs_to_zone:
+ Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+ (** Evaluation of the memory zone written by an assigns clauses, in the given
+ cvalue state. *)
+ val assigns_outputs_to_zone:
+ result: Cil_types.varinfo option ->
+ Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
(** 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/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 64edb349ce73906c2350ffd7a664064ea8fc099d..8d6cd7d02787c84b7086f9d726ad9d48d2118dbd 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -22,6 +22,68 @@
open Cil_types
+let valid_behaviors kf state =
+ let funspec = Annotations.funspec kf in
+ let eval_predicate pred =
+ match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
+ | True -> Alarmset.True
+ | False -> Alarmset.False
+ | Unknown -> Alarmset.Unknown
+ in
+ let ab = Active_behaviors.create eval_predicate funspec in
+ Active_behaviors.active_behaviors ab
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute inout from assigns clauses --- *)
+(* -------------------------------------------------------------------------- *)
+
+let eval_error_reason fmt e =
+ if e <> Eval_terms.CAlarm
+ then Eval_terms.pretty_logic_evaluation_error fmt e
+
+let eval_tlval_as_zone assigns kind env acc t =
+ try
+ let alarm_mode = Eval_terms.Ignore in
+ let zone = Eval_terms.eval_tlval_as_zone ~alarm_mode kind env t.it_content in
+ Locations.Zone.join acc zone
+ with Eval_terms.LogicEvalError e ->
+ let pp_clause fmt =
+ if kind = Read
+ then Printer.pp_from fmt assigns
+ else Printer.pp_term fmt (fst assigns).it_content
+ in
+ Self.warning ~current:true ~once:true
+ "Failed to interpret %sassigns clause '%t'%a"
+ (if kind = Read then "inputs in " else "")
+ pp_clause eval_error_reason e;
+ Locations.Zone.top
+
+let assigns_inputs_to_zone state assigns =
+ let env = Eval_terms.env_assigns ~pre:state in
+ let treat_asgn acc (_,ins as asgn) =
+ match ins with
+ | FromAny -> Locations.Zone.top
+ | From l -> List.fold_left (eval_tlval_as_zone asgn Read env) acc l
+ in
+ match assigns with
+ | WritesAny -> Locations.Zone.top
+ | Writes l -> List.fold_left treat_asgn Locations.Zone.bottom l
+
+let assigns_outputs_to_zone ~result state assigns =
+ let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
+ let treat_asgn acc (out,_ as asgn) =
+ if Logic_utils.is_result out.it_content && result = None
+ then acc
+ else eval_tlval_as_zone asgn Write env acc out
+ in
+ match assigns with
+ | WritesAny -> Locations.Zone.top
+ | Writes l -> List.fold_left treat_asgn Locations.Zone.bottom l
+
+(* -------------------------------------------------------------------------- *)
+(* --- Verify assigns clauses --- *)
+(* -------------------------------------------------------------------------- *)
+
(* Eval: under-approximation of the term. Note that ACSL states
that assigns clauses are evaluated in the pre-state.
We skip [\result]: it is meaningless when evaluating the 'assigns' part,
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index f29202c96c739e9ae8d939674510a52ddfbb0425..f26ba262e163603ad15adff669524b8d83fa91d4 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -22,6 +22,22 @@
[@@@ api_start]
+(** Returns the list of behaviors of the given function that are active for
+ the given initial state. *)
+val valid_behaviors:
+ Cil_types.kernel_function -> Cvalue.Model.t -> Cil_types.behavior list
+
+(** Evaluation of the memory zone read by the \from part of an assigns clause,
+ in the given cvalue state. *)
+val assigns_inputs_to_zone:
+ Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
+(** Evaluation of the memory zone written by an assigns clauses, in the given
+ cvalue state. *)
+val assigns_outputs_to_zone:
+ result: Cil_types.varinfo option ->
+ Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+
(** 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/register.ml b/src/plugins/eva/register.ml
index d216a3abb25084c1526df8258b1ead0cdf93e73e..197393e0a5592251d9aaf9201d072a6e3617a309 100644
--- a/src/plugins/eva/register.ml
+++ b/src/plugins/eva/register.ml
@@ -34,76 +34,6 @@ let main () =
let () = Db.Main.extend main
-(* Functions to register in Db.Value *)
-
-let eval_error_reason fmt e =
- if e <> Eval_terms.CAlarm
- then Eval_terms.pretty_logic_evaluation_error fmt e
-
-let assigns_inputs_to_zone state assigns =
- let env = Eval_terms.env_assigns ~pre:state in
- let treat_asgn acc (_,ins as asgn) =
- match ins with
- | FromAny -> Zone.top
- | From l ->
- try
- List.fold_left
- (fun acc t ->
- let z =
- Eval_terms.eval_tlval_as_zone ~alarm_mode:Eval_terms.Ignore
- Read env t.it_content
- in
- Zone.join acc z)
- acc
- l
- with Eval_terms.LogicEvalError e ->
- Self.warning ~current:true ~once:true
- "Failed to interpret inputs in assigns clause '%a'%a"
- Printer.pp_from asgn eval_error_reason e;
- Zone.top
- in
- match assigns with
- | WritesAny -> Zone.top
- | Writes l -> List.fold_left treat_asgn Zone.bottom l
-
-let assigns_outputs_aux ~eval ~bot ~top ~join state ~result assigns =
- let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
- let treat_asgn acc ({it_content = out},_) =
- if Logic_utils.is_result out && result = None
- then acc
- else
- try
- let z = eval env out in
- join z acc
- with Eval_terms.LogicEvalError e ->
- Self.warning ~current:true ~once:true
- "Failed to interpret assigns clause '%a'%a"
- Printer.pp_term out eval_error_reason e;
- join top acc
- in
- match assigns with
- | WritesAny -> join top bot
- | Writes l -> List.fold_left treat_asgn bot l
-
-let assigns_outputs_to_zone =
- let eval env term =
- Eval_terms.eval_tlval_as_zone
- ~alarm_mode:Eval_terms.Ignore Write env term
- in
- assigns_outputs_aux ~eval
- ~bot:Locations.Zone.bottom ~top:Locations.Zone.top ~join:Locations.Zone.join
-
-let assigns_outputs_to_locations =
- let eval env term =
- Eval_terms.eval_tlval_as_location
- ~alarm_mode:Eval_terms.Ignore env term
- in
- assigns_outputs_aux
- ~eval
- ~bot:[] ~top:(Locations.make_loc Locations.Location_Bits.top Int_Base.top)
- ~join:(fun v l -> v :: l)
-
-
(* "access" functions before evaluation, registered in Db.Value *)
let access_value_of_lval kinstr lv =
let state = Db.Value.get_state kinstr in
@@ -132,30 +62,19 @@ let eval_predicate ~pre ~here p =
| False -> Property_status.False_if_reachable
| Unknown -> Property_status.Dont_know
-let valid_behaviors kf state =
- let funspec = Annotations.funspec kf in
- let eval_predicate pred =
- match Eval_terms.(eval_predicate (env_pre_f ~pre:state ()) pred) with
- | Eval_terms.True -> Alarmset.True
- | Eval_terms.False -> Alarmset.False
- | Eval_terms.Unknown -> Alarmset.Unknown
- in
- let ab = Active_behaviors.create eval_predicate funspec in
- Active_behaviors.active_behaviors ab
-
let () =
Db.Value.is_called := Function_calls.is_called;
Db.Value.callers := Function_calls.callsites;
Db.Value.use_spec_instead_of_definition :=
Function_calls.use_spec_instead_of_definition;
- Db.Value.assigns_outputs_to_zone := assigns_outputs_to_zone;
- Db.Value.assigns_outputs_to_locations := assigns_outputs_to_locations;
- Db.Value.assigns_inputs_to_zone := assigns_inputs_to_zone;
+ Db.Value.assigns_outputs_to_zone :=
+ (fun s ~result a -> Logic_inout.assigns_outputs_to_zone ~result s a);
+ Db.Value.assigns_inputs_to_zone := Logic_inout.assigns_inputs_to_zone;
Db.Value.access := access_value_of_lval;
Db.Value.access_location := access_value_of_location;
Db.Value.access_expr := access_value_of_expr;
Db.Value.Logic.eval_predicate := eval_predicate;
- Db.Value.valid_behaviors := valid_behaviors;
+ Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
Db.From.find_deps_term_no_transitivity_state :=
find_deps_term_no_transitivity_state;