[Eva] allows to ask the state after the stmt

  - TODO for Cvalue

.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

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

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

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

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 =