diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index baad021381a46b3905e7a24582131c9f33fa833c..7a20c4877889d8db02b065264b805a023b1eb8f1 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -316,6 +316,13 @@ module Value = struct
let size = size
let dependencies = [ Table_By_Callstack.self ]
end)
+ module AfterTable =
+ Cil_state_builder.Stmt_hashtbl(Cvalue.Model)
+ (struct
+ let name = "Db.Value.AfterTable"
+ let size = size
+ let dependencies = [ AfterTable_By_Callstack.self ]
+ end)
let self = Table_By_Callstack.self
@@ -519,13 +526,21 @@ module Value = struct
let add_formals_to_state = mk_fun "add_formals_to_state"
- let noassert_get_stmt_state s =
+ let noassert_get_stmt_state ~after s =
if !no_results (Kernel_function.(get_definition (find_englobing_kf s)))
then Cvalue.Model.top
else
- try Table.find s
+ let tbl : (module State_builder.Hashtbl with type key = Cil_types.stmt
+ and type data = Cvalue.Model.t) =
+ if after then (module AfterTable) else (module Table) in
+ let module Tbl = (val tbl) in
+ try Tbl.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 s else
+ Table_By_Callstack.find s)
+ with Not_found -> None in
let state =
match ho with
| None -> Cvalue.Model.bottom
@@ -534,21 +549,24 @@ module Value = struct
Cvalue.Model.join acc state
) h Cvalue.Model.bottom
in
- Table.add s state;
+ Tbl.add s state;
state
- let noassert_get_state k =
+ let noassert_get_state ?(after=false) k =
match k with
| Kglobal -> globals_state ()
- | Kstmt s -> noassert_get_stmt_state s
+ | Kstmt s ->
+ noassert_get_stmt_state ~after s
- let get_stmt_state s =
+ let get_stmt_state ?(after=false) s =
+ (* [QB]: false was previous default. *)
assert (is_computed ()); (* this assertion fails during value analysis *)
- noassert_get_stmt_state s
+ noassert_get_stmt_state ~after s
- let get_state k =
+ let get_state ?(after=false) k =
+ (* [QB]: false was previous default. *)
assert (is_computed ()); (* this assertion fails during value analysis *)
- noassert_get_state k
+ noassert_get_state ~after k
let get_stmt_state_callstack ~after stmt =
assert (is_computed ()); (* this assertion fails during value analysis *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index cd627fbe6855a4390136b3cd1228a135511f32a5..74f81d2081793e1c6c6101127a1ffec15c10ff83 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -265,13 +265,13 @@ module Value : sig
val get_initial_state : kernel_function -> state
val get_initial_state_callstack :
kernel_function -> state Value_types.Callstack.Hashtbl.t option
- val get_state : kinstr -> state
+ val get_state : ?after:bool -> kinstr -> state
val get_stmt_state_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t option
- val get_stmt_state : stmt -> state
+ val get_stmt_state : ?after:bool -> stmt -> state
(** @plugin development guide *)
val fold_stmt_state_callstack :
@@ -519,7 +519,7 @@ module Value : sig
(**/**)
(** {3 Internal use only} *)
- val noassert_get_state : kinstr -> state
+ val noassert_get_state : ?after:bool -> kinstr -> state
(** To be used during the value analysis itself (instead of
{!get_state}). *)
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 66d83674fe4205892624c5fdf2c01c365a269c53..3233b733bfc3f559d3062b8e4af0aa3769affb49 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -37,7 +37,7 @@ let () = From_parameters.ForceDeps.set_output_dependencies [Tbl.self]
let force_compute = ref (fun _ -> assert false)
module To_Use = struct
- let get_value_state = Db.Value.get_stmt_state
+ let get_value_state s = Db.Value.get_stmt_state s
let memo kf =
Tbl.memo
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 1c070d2ddf96a72f356d251e2394de36da5f4ced..3df4c0086321b7029848e3f25d6b536634a12e38 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -699,7 +699,7 @@ module FunctionWise = struct
let module Computer = Computer(Fenv)(struct
let _version = "functionwise"
let _kf = kf
- let stmt_state = Db.Value.get_stmt_state
+ let stmt_state s = Db.Value.get_stmt_state s
let at_call stmt kf = get_external_aux ~stmt kf
end) in
Stack.iter
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 4a1da6a935249339f8acfae70e3ef774e21dba0c..ca999ade6757a6fe4f168d1ac5f72226ccfae2a0 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: ?after:bool -> 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 f3b0fe3d1c8f3263ed3df950a1b661e736f3654a..841850c4fefb3bc6b3bc6b678eefa8887bf517fa 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -473,7 +473,9 @@ module State = struct
| None -> `Bottom
else `Top
- let get_stmt_state ?(after=false) stmt = assert (not after); return (Db.Value.get_stmt_state stmt)
+ let get_stmt_state ~after stmt =
+ return (Db.Value.get_stmt_state ~after 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 d75ccc84f229c387a4f9b4fa66711d38caf205ef..e596deec5d4fb9c3ec0864d3e1db015137fa16de 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 ?after stmt =
- Left.Store.get_stmt_state ?after stmt >>- fun left ->
- Right.Store.get_stmt_state ?after 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 2341f4e22a0208fedda7a128995a477c6b0494f1..150129f159c2c4e1e057d5ea72930625807ee6a9 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -208,7 +208,7 @@ module Make (Domain: InputDomain) = struct
try `Value (Called_Functions_By_Callstack.find kf)
with Not_found -> `Bottom
- let get_stmt_state ?(after=false) s =
+ let get_stmt_state ~after s =
if not (Storage.get ())
then `Value Domain.top
else
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 14728aa4d7eee27bada599f8273025a4b5c1925e..fd3cf68003bf90f49e026ed3028488d18cf19c72 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -28,8 +28,8 @@ module type Results = sig
type value
type location
- val get_stmt_state : stmt -> state or_bottom
- val get_kinstr_state: kinstr -> state or_bottom
+ val get_stmt_state : after:bool -> stmt -> state or_bottom
+ val get_kinstr_state: after:bool -> kinstr -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
val get_initial_state_by_callstack:
@@ -67,15 +67,15 @@ module Make (Abstract: Abstractions.S) = struct
include Abstract
include Compute_functions.Make (Abstract)
- let get_stmt_state stmt =
+ let get_stmt_state ~after stmt =
let fundec = Kernel_function.(get_definition (find_englobing_kf stmt)) in
if Mark_noresults.should_memorize_function fundec && Db.Value.is_computed ()
- then Abstract.Dom.Store.get_stmt_state stmt
+ then Abstract.Dom.Store.get_stmt_state ~after stmt
else `Value Abstract.Dom.top
- let get_kinstr_state = function
+ let get_kinstr_state ~after = function
| Kglobal -> Abstract.Dom.Store.get_global_state ()
- | Kstmt stmt -> get_stmt_state stmt
+ | Kstmt stmt -> get_stmt_state ~after stmt
let get_stmt_state_by_callstack =
Abstract.Dom.Store.get_stmt_state_by_callstack
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 4ecfde378fd0c90f6ca56c0bb9c93909e95c18d6..89316e76c4cf49ddc2b26d495f46097f64517870 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -28,8 +28,8 @@ module type Results = sig
type value
type location
- val get_stmt_state : stmt -> state or_bottom
- val get_kinstr_state: kinstr -> state or_bottom
+ val get_stmt_state : after:bool -> stmt -> state or_bottom
+ val get_kinstr_state: after:bool -> kinstr -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
val get_initial_state_by_callstack:
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index d455fab0fdc74a67016f135cf4e9ccbb67be4738..7892476419f1a383686204648a6668674b6dbd21 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -519,7 +519,7 @@ module Select (Eval: Eval) = struct
(* Function pointers *)
(* get the list of functions in the values *)
let e = Value_util.lval_to_exp lv in
- match Eval.Analysis.get_kinstr_state ki with
+ match Eval.Analysis.get_kinstr_state ~after:false ki with
| `Bottom -> ()
| `Value state ->
let funs, _ = Eval.Analysis.eval_function_exp state e in