From a564d362f9967d0a14ff480afc8f93ad850bfcdb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 29 Sep 2017 11:07:41 +0200
Subject: [PATCH] [Eva] allows to ask the state after the stmt
- TODO for Cvalue
---
.gitignore | 5 ++---
src/plugins/value/domains/abstract_domain.mli | 2 +-
.../value/domains/cvalue/cvalue_domain.ml | 2 +-
src/plugins/value/domains/domain_product.ml | 6 +++---
src/plugins/value/domains/domain_store.ml | 16 ++++++++++++----
5 files changed, 19 insertions(+), 12 deletions(-)
diff --git a/.gitignore b/.gitignore
index 0e333030f4d..1b62026db65 100644
--- a/.gitignore
+++ b/.gitignore
@@ -42,9 +42,8 @@ autom4te.cache
#tests
/tests/ptests_config
-/tests/*/result/
-/tests/*/*/result/
-/tests/*/result_*/
+/tests/**/result/
+/tests/**/result_*/
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index ae2c25c9722..4a1da6a9352 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -481,7 +481,7 @@ module type Store = sig
val get_initial_state_by_callstack:
kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
- val get_stmt_state: stmt -> state or_bottom
+ val get_stmt_state: ?after:bool -> stmt -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
end
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 995298130d6..f3b0fe3d1c8 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -473,7 +473,7 @@ module State = struct
| None -> `Bottom
else `Top
- let get_stmt_state stmt = return (Db.Value.get_stmt_state stmt)
+ let get_stmt_state ?(after=false) stmt = assert (not after); return (Db.Value.get_stmt_state stmt)
let get_stmt_state_by_callstack ~after stmt =
if Storage.get ()
then
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index fffc784d6c8..d75ccc84f22 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -366,9 +366,9 @@ module Make
and right_tbl = Right.Store.get_initial_state_by_callstack kf in
merge_callstack_tbl left_tbl right_tbl
- let get_stmt_state stmt =
- Left.Store.get_stmt_state stmt >>- fun left ->
- Right.Store.get_stmt_state stmt >>-: fun right ->
+ let get_stmt_state ?after stmt =
+ Left.Store.get_stmt_state ?after stmt >>- fun left ->
+ Right.Store.get_stmt_state ?after stmt >>-: fun right ->
left, right
let get_stmt_state_by_callstack ~after stmt =
let left_tbl = Left.Store.get_stmt_state_by_callstack ~after stmt
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index 6bcf2d60866..2341f4e22a0 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -104,6 +104,13 @@ module Make (Domain: InputDomain) = struct
let size = size
let dependencies = dependencies
end)
+ module AfterTable =
+ Cil_state_builder.Stmt_hashtbl (Domain)
+ (struct
+ let name = name ^ ".AfterTable"
+ let size = size
+ let dependencies = [ AfterTable_By_Callstack.self ]
+ end)
module Called_Functions_By_Callstack =
State_builder.Hashtbl
@@ -201,13 +208,14 @@ module Make (Domain: InputDomain) = struct
try `Value (Called_Functions_By_Callstack.find kf)
with Not_found -> `Bottom
- let get_stmt_state s =
+ let get_stmt_state ?(after=false) s =
if not (Storage.get ())
then `Value Domain.top
else
- try `Value (Table.find s)
+ try `Value ((if after then AfterTable.find else Table.find) s)
with Not_found ->
- let ho = try Some (Table_By_Callstack.find s) with Not_found -> None in
+ let ho = try Some ((if after then AfterTable_By_Callstack.find
+ else Table_By_Callstack.find) s) with Not_found -> None in
let state =
match ho with
| None -> `Bottom
@@ -216,7 +224,7 @@ module Make (Domain: InputDomain) = struct
(fun _cs state acc -> Bottom.join Domain.join acc (`Value state))
h `Bottom
in
- ignore (state >>-: Table.add s);
+ ignore (state >>-: (if after then AfterTable.add else Table.add) s);
state
let get_stmt_state_by_callstack ~after stmt =
--
GitLab