diff --git a/.gitignore b/.gitignore index 0e333030f4d2f99767fd4ca245b5c91ccbfd7f55..1b62026db65f526f2fbbd80f37d092e8d7eac723 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 ae2c25c97226fb9ec33e2b24d1ba08eb68f4752e..4a1da6a935249339f8acfae70e3ef774e21dba0c 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 995298130d6c76007449e4477f00dbb2b82b3439..f3b0fe3d1c8f3263ed3df950a1b661e736f3654a 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 fffc784d6c8ec628b931a200e587caf909a8c86c..d75ccc84f229c387a4f9b4fa66711d38caf205ef 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 6bcf2d60866172e9f4e3e0889fa671f5c0d0dec4..2341f4e22a0208fedda7a128995a477c6b0494f1 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 =