From 23beef9115a5abe994ab9d9924ac77e76aea8846 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 13 Oct 2022 16:35:53 +0200
Subject: [PATCH] [Eva] Exports Db.Properties.loc_to_loc as
Eva_results.eval_tlval_as_location
---
src/plugins/eva/Eva.mli | 4 ++++
src/plugins/eva/utils/eva_results.ml | 4 ++++
src/plugins/eva/utils/eva_results.mli | 4 ++++
3 files changed, 12 insertions(+)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 3b01353a856..d36e2198c59 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -727,6 +727,10 @@ module Eva_results: sig
val change_callstacks:
(Value_types.callstack -> Value_types.callstack) -> results -> results
+ val eval_tlval_as_location :
+ ?result:Cil_types.varinfo ->
+ Cvalue.Model.t -> Cil_types.term -> Locations.location
+
end
module Unit_tests: sig
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index fcdde083d16..0d89c3a001b 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -263,6 +263,10 @@ let merge r1 r2 =
{ main; before_states; after_states; kf_initial_states;
initial_state; initial_args; alarms; statuses; kf_callers }
+let eval_tlval_as_location ?result state term =
+ let env = Eval_terms.env_post_f ~pre:state ~post:state ~result () in
+ try Eval_terms.eval_tlval_as_location ~alarm_mode:Ignore env term
+ with Eval_terms.LogicEvalError _ -> raise Logic_to_c.No_conversion
(*
Local Variables:
diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli
index 19e35f6bd7b..ca502d65f62 100644
--- a/src/plugins/eva/utils/eva_results.mli
+++ b/src/plugins/eva/utils/eva_results.mli
@@ -46,6 +46,10 @@ val merge: results -> results -> results
val change_callstacks:
(Value_types.callstack -> Value_types.callstack) -> results -> results
+val eval_tlval_as_location :
+ ?result:Cil_types.varinfo ->
+ Cvalue.Model.t -> Cil_types.term -> Locations.location
+
[@@@ api_end]
(*
--
GitLab