diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 9d3ca7a464991e0992fdadc31eea6163f1c7caad..f112996ac4771ed771ee90d64027b2b8fdf3b54a 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -352,7 +352,6 @@ let ival_to_interval = function
module type Input = sig
type t
val manager: t Manager.t
- val name: string
end
module Make (Man : Input) = struct
@@ -404,8 +403,6 @@ module Make (Man : Input) = struct
end )
include D
- let name = Man.name
-
let is_included = Abstract1.is_leq man
let join s1 s2 =
@@ -432,7 +429,6 @@ module Make (Man : Input) = struct
include Domain_builder.Complete
(struct
include D
- let name = name
let top = top
let join = join
end)
@@ -694,29 +690,24 @@ end
module Apron_Octagon = struct
type t = Oct.t
let manager = Oct.manager_alloc ()
- let name = "apron-octagon"
end
module Apron_Box = struct
type t = Box.t
let manager = Box.manager_alloc ()
- let name = "apron-box"
end
module Apron_Polka_Loose = struct
type t = Polka.loose Polka.t
let manager = Polka.manager_alloc_loose ()
- let name = "apron-polka-loose"
end
module Apron_Polka_Strict = struct
type t = Polka.strict Polka.t
let manager = Polka.manager_alloc_strict ()
- let name = "apron-polka-strict"
end
module Apron_Polka_Equalities = struct
type t = Polka.equalities Polka.t
let manager = Polka.manager_alloc_equalities ()
- let name = "apron-polka-equality"
end
(** Apron manager allocation changes the rounding mode. *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index b7a0e91e222ed6ae6dd9bac88adbd825c8275b6d..a3df62f2573a7b8ff88db80cbc414386661d40c3 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -181,7 +181,6 @@ module State = struct
let mem_project = Datatype.never_any_project
end )
- let name = "cvalue"
let key = Structure.Key_Domain.create_key "cvalue_domain"
type value = Model.value
@@ -455,7 +454,7 @@ module State = struct
let default () = false
end)
- let register_global_state _ = Storage.set true
+ let register_global_state _ _ = Storage.set true
let register_initial_state callstack (state, _clob) =
Db.Value.merge_initial_state callstack state
let register_state_before_stmt callstack stmt (state, _clob) =
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index d92cfab71441b6f634fcb5360dfd4020ee93322f..6cb8e354211b850892dce2349e090c84685d0c82 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -589,9 +589,9 @@ module Restrict
module Store = struct
- let register_global_state state =
+ let register_global_state b state =
let state = state >>-: get_state in
- Domain.Store.register_global_state state
+ Domain.Store.register_global_state b state
let lift_register f state = f (get_state state)
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 4ea88b8b41f51be54b2ec089efb36e4f948599ed..79ceb9c587690a7761c99512194dc65410aea209 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -324,9 +324,9 @@ module Make
| `Bottom, _ | _, `Bottom -> `Bottom
module Store = struct
- let register_global_state state =
- Left.Store.register_global_state (state >>-: fst);
- Right.Store.register_global_state (state >>-: snd)
+ let register_global_state b state =
+ Left.Store.register_global_state b (state >>-: fst);
+ Right.Store.register_global_state b (state >>-: snd)
let register_initial_state callstack (left, right) =
Left.Store.register_initial_state callstack left;
Right.Store.register_initial_state callstack right
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index c33e654ebac25a48a16f4920b28aced12633915d..23cf9353b87323f8148c8addb91e02a382b4ef98 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -31,7 +31,7 @@ end
module type S = sig
type t
- val register_global_state: t or_bottom -> unit
+ val register_global_state: bool -> t or_bottom -> unit
val register_initial_state: Value_types.callstack -> t -> unit
val register_state_before_stmt: Value_types.callstack -> stmt -> t -> unit
val register_state_after_stmt: Value_types.callstack -> stmt -> t -> unit
@@ -172,8 +172,7 @@ module Make (Domain: InputDomain) = struct
Callstack.Hashtbl.add r callstack v;
add stmt r
- let register_global_state state =
- let storage = not (Value_parameters.NoResultsDomains.mem Domain.name) in
+ let register_global_state storage state =
Storage.set storage;
if storage then
match state with
diff --git a/src/plugins/value/domains/domain_store.mli b/src/plugins/value/domains/domain_store.mli
index 136b3ba458e7c139859b58e02b73a88b37ecbe2c..fd9ddfd450d4664b3e8b764472396b47def5425c 100644
--- a/src/plugins/value/domains/domain_store.mli
+++ b/src/plugins/value/domains/domain_store.mli
@@ -32,7 +32,13 @@ end
(** Automatic storage of the states computed during the analysis. *)
module type S = sig
type t
- val register_global_state: t or_bottom -> unit
+
+ (** Called once at the analysis beginning for the entry state of the main
+ function. The boolean indicates whether the states of this domain must be
+ saved during the analysis, according to options -eva-no-results. If it is
+ false, register functions must do nothing, and get functions return Top. *)
+ val register_global_state: bool -> t or_bottom -> unit
+
val register_initial_state: Value_types.callstack -> t -> unit
val register_state_before_stmt: Value_types.callstack -> stmt -> t -> unit
val register_state_after_stmt: Value_types.callstack -> stmt -> t -> unit
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 2d02024b041d7a9da3fa650fee269ec5cdcf69d6..e345ba15493770b7cfdb46f083704e135d192adc 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -121,7 +121,6 @@ module Internal = struct
type state = t
- let name = "equality"
let log_category = dkey
let key = Structure.Key_Domain.create_key "equality_domain"
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index cb2df307734d7966757fdad3a11efe9dc65c5f3e..3d5c2e301910c79a81d237a12e3d444a3e1d06b5 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -538,8 +538,6 @@ module G = struct
(Datatype.List(Datatype.Pair(Cil_datatype.Stmt)(IterationInfo)))
(struct let module_name = "Values.Gauges_domain.G" end)
- let name = "gauges"
-
let empty = MV.empty, []
let top (state: t) : t =
let top_iteration_info = function
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 4dcf4b41c1782c598c3ba76c79e8489e843f8a1a..946b34461d059ea28d0c5cbc00a844d411cb9ef8 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -95,8 +95,6 @@ module LatticeInout = struct
end)
- let name = "inout"
-
(* Initial abstract at the beginning of the computation: nothing written
or read so far. *)
let empty = {
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 98f7f2f7912828a6aff1c715e8de2c1db90cd344..90abdbb2f7bdaa9de528c55ec6cdeedf28a25d4b 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -241,7 +241,6 @@ struct
(Base.Base) (Memory)
(Hptmap.Comp_unused) (Initial_Values) (Deps)
- let name = "multidim"
let log_category = dkey
let cache_name s =
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 66376372155e74518a3119e93d3775292bdc0cec..b8968a5f1396f409525488716e457c1baa70c8b9 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -753,7 +753,6 @@ module State = struct
Format.fprintf fmt "@[%a@]" Octagons.pretty octagons
end)
- let name = "octagon"
let log_category = Value_parameters.register_category "d-octagon"
let pretty_debug fmt { octagons; intervals; relations } =
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 826c01725abbc568b849820225fbdb31ec15cbf8..235d98ba9909b29645acd381f1348c3704a07685 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -86,8 +86,6 @@ module Memory = struct
widen wh s1 s2
let narrow x _y = `Value x
-
- let name = "bitwise"
end
diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml
index c550a08af7aa618a1631aa5739c9d5c8b9f6d50a..0be9f3fb61d85bd030a328335354874f295f89e8 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -34,7 +34,6 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
(* In this domain, the states contain nothing. We use [unit] as type formal
the state and we reuse [Datatype.Unit] as a base for our domain. *)
include Datatype.Unit
- let name = "printer"
(* --- Lattice operators --- *)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 1e44803fbcedb5194f0cbd280b6d25ddacee8e48..fa09688306a1d5aff2d62bad75740884394c2306 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -191,8 +191,6 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
include Domain_builder.Complete (M)
- let name = Info.name
-
type state = t
type value = Value.t
type location = Precise_locs.precise_location
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 2c854e7797765c1427a6930d287679ab02d1e1a2..f4d8f92b93d475b10f090a70f2140f5460f005e0 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -215,8 +215,6 @@ module Memory = struct
end)
- let name = "symbolic-locations"
-
let top = {
values = K2V.M.empty;
zones = K2Z.empty;
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 53d5dcd618f76b334749aa276188ca923f5bb532..aec330a279eb299accb535ee05b8e4a1830f53b2 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -106,8 +106,6 @@ module LatticeTaint = struct
end)
- let name = "taint"
-
(* Initial state at the start of the computation: nothing is tainted yet. *)
let empty = {
locs_data = Zone.bottom;
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 20918ad9f2c2ff095442ffcb1b20debfa08416cb..88ccb4412c530ed6713e09d7eac5739dbddbde61 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -571,8 +571,6 @@ module Traces = struct
end)
- let name = "traces"
-
let view m =
if m == top then `Top
else `Other m
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 4497123b4939d86b5fd792333827c942b3db319c..3915bb1a4f03312460bac11e739727a691ff7ad6 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -323,7 +323,7 @@ let eq_value:
| Abstract.Value.Leaf (key, _) -> Abstract.Value.eq_type key V.key
| _ -> None
-let add_domain (type v) mode (abstraction: v abstraction) (module Acc: Acc) =
+let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc) =
let domain : (module internal_domain with type value = Acc.Val.t) =
match abstraction.domain with
| Functor make ->
@@ -343,15 +343,27 @@ let add_domain (type v) mode (abstraction: v abstraction) (module Acc: Acc) =
let module Convert = Internal_Value.Convert (Acc.Val) (Struct) in
(module Domain_lift.Make (Domain) (Convert))
in
+ (* Set the name of the domain. *)
+ let module Domain = struct
+ include (val domain)
+ let name = dname
+ module Store = struct
+ include Store
+ let register_global_state storage state =
+ let no_results = Value_parameters.NoResultsDomains.mem dname in
+ register_global_state (storage && not no_results) state
+ end
+ end in
+ (* Restricts the domain according to [mode]. *)
let domain : (module internal_domain with type value = Acc.Val.t) =
match mode with
- | None -> domain
+ | None -> (module Domain)
| Some kf_modes ->
let module Scope = struct let functions = kf_modes end in
let module Domain =
Domain_builder.Restrict
(Acc.Val)
- ((val domain))
+ (Domain)
(Scope)
in
(module Domain)
@@ -378,7 +390,7 @@ let warn_experimental flag =
let build_domain config abstract =
let build (Flag flag, mode) acc =
warn_experimental flag;
- add_domain mode flag.abstraction acc
+ add_domain flag.name mode flag.abstraction acc
in
(* Domains in the [config] are sorted by increasing priority: domains with
higher priority are added last: they will be at the top of the domains
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index ece699c60df2f50dfa57448e281799a191c9e1f8..4d517e199e2d2d44ea209f1a875ec0cf0d17a054 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -375,7 +375,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_from_init_state kf init_state =
pre_analysis ();
- Abstract.Dom.Store.register_global_state (`Value init_state);
+ let b = Value_parameters.ResultsAll.get () in
+ Abstract.Dom.Store.register_global_state b (`Value init_state);
compute kf init_state
end
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index 2be609d248deefa31267b01fa294f57f0c96186d..eacfe860a70ae2f7fcf39af02fed264399c8a898 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -397,7 +397,8 @@ module Make
state
end
in
- Domain.Store.register_global_state init_state;
+ let b = Value_parameters.ResultsAll.get () in
+ Domain.Store.register_global_state b init_state;
print_initial_cvalue_state init_state;
init_state >>-: add_main_formals kf