diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli index e8536eb1f6e16c262d723f096cf919917e47eb29..255d42d7ecda023e34deda8ded277f9adbb6cfed 100644 --- a/src/plugins/value/domains/abstract_domain.mli +++ b/src/plugins/value/domains/abstract_domain.mli @@ -376,6 +376,10 @@ module type S = sig type state include Datatype.S_with_collections with type t = state + (* The domain name, shown in some logs and in the GUI. Be sure to redefine a + clear and simple name instead of the default one coming from Datatype. *) + val name: string + (** {3 Lattice Structure } *) include Lattice with type state := t diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml index 77f90be12ff69cc314f8da40cba6f39990e344c1..5a81d35d4f1d8fa60e7a8d701603c6023c096c38 100644 --- a/src/plugins/value/domains/cvalue/cvalue_domain.ml +++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml @@ -181,7 +181,8 @@ module State = struct let mem_project = Datatype.never_any_project end ) - let key = Structure.Key_Domain.create_key "cvalue_domain" + let name = "cvalue" + let key = Structure.Key_Domain.create_key name type value = Model.value type location = Model.location diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml index 141c643cc703d84b082afa5a7af9e5b6355a0b92..6eadb1af7c204b8a9dc5b19f009acbc01aec4d02 100644 --- a/src/plugins/value/domains/domain_builder.ml +++ b/src/plugins/value/domains/domain_builder.ml @@ -325,6 +325,7 @@ module Restrict module I = struct let module_name = Domain.name ^ " option" end include Datatype.Option_with_collections (D) (I) + let name = Domain.name let default = Domain.top, Mode.all let structure: t Abstract.Domain.structure = diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli index bf3c05b8f0cc79efed1e2e4ec30131f737bd49df..bd0fd0c5f2491c840290773b808e39af4d594cb3 100644 --- a/src/plugins/value/domains/domain_builder.mli +++ b/src/plugins/value/domains/domain_builder.mli @@ -27,6 +27,8 @@ open Cil_types open Eval module type InputDomain = sig + (* The [name] value from Datatype should be the domain name and will be used + in some logs and in the GUI for the end-user. *) include Datatype.S val top: t val join: t -> t -> t diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml index 550a86f3d45fd987f474e297732ee21553b1f157..e158cb43b035938d00e5c63e158e8641af291b66 100644 --- a/src/plugins/value/domains/domain_product.ml +++ b/src/plugins/value/domains/domain_product.ml @@ -42,14 +42,15 @@ module Make } let () = incr counter - let name = Left.name ^ "*" ^ Right.name ^ - "(" ^ string_of_int !counter ^ ")" + let unique_name = Left.name ^ "*" ^ Right.name ^ + "(" ^ string_of_int !counter ^ ")" include Datatype.Pair_with_collections (Left) (Right) - (struct let module_name = name end) + (struct let module_name = unique_name end) type state = t + let name = Left.name ^ " * " ^ Right.name let structure = Abstract.Domain.Node (Left.structure, Right.structure) diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml index 44604b43c15df1ff2c12a3940b0d0d745d580dff..542d48cc2ce424ece24b54e1cdfc07a6428bab75 100644 --- a/src/plugins/value/domains/equality/equality_domain.ml +++ b/src/plugins/value/domains/equality/equality_domain.ml @@ -121,6 +121,8 @@ module Internal = struct type state = t + let name = "equality" + let log_category = dkey let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml index 7a91a6af3f8e2dc22c04e88287d12316f2853dd0..829afa083647c8d8e174c8e8c3a1303b840df1c9 100644 --- a/src/plugins/value/domains/gauges/gauges_domain.ml +++ b/src/plugins/value/domains/gauges/gauges_domain.ml @@ -532,6 +532,8 @@ 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 8028b618a1d7e5df61659ebd87c72c7921f8ab96..63af3599eafb50965cc660d38e85473fa0d0a957 100644 --- a/src/plugins/value/domains/inout_domain.ml +++ b/src/plugins/value/domains/inout_domain.ml @@ -44,7 +44,7 @@ module LatticeInout = struct include Datatype.Serializable_undefined type t = inout - let name = "Value.Inout.t" + let name = "inout" let reprs = [ { over_outputs = List.hd Zone.reprs; diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml index 2f6459d9c5c63631f202e43bf47504a6dfb34690..0a65d601baf128e4951680d8c74ee0cea2929646 100644 --- a/src/plugins/value/domains/multidim/multidim_domain.ml +++ b/src/plugins/value/domains/multidim/multidim_domain.ml @@ -363,6 +363,8 @@ struct (Datatype.Option (Tracking)) (struct let module_name = "DomainLattice" end) + let name = "multidim" + type state = t type value = Value.t type value_or_uninitialized = Value_or_Uninitialized.t diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml index 757ad4d87ecadaba7e9b0bfe9fa985c413fba7f6..b96b6bb17a55b8d2a78031892631cb177e4a0154 100644 --- a/src/plugins/value/domains/octagons.ml +++ b/src/plugins/value/domains/octagons.ml @@ -701,7 +701,7 @@ module State = struct type t = state include Datatype.Serializable_undefined - let name = "Octagons.State" + let name = "octagon" let structural_descr = Structural_descr.t_record [| Octagons.packed_descr; diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml index 66ffd1337c2b6e88dd72b51d5fbc08a9ccea7c64..65d6d1a2f6d4f6592ffb2350b9d7ffc023deff65 100644 --- a/src/plugins/value/domains/offsm_domain.ml +++ b/src/plugins/value/domains/offsm_domain.ml @@ -81,6 +81,8 @@ module Memory = struct include Lmap.Make_LOffset(V_Or_Uninitialized)(V_Offsetmap)(Default_offsetmap) + let name = "bitwise" + let widen kf stmt s1 s2 = let wh = Widen.getWidenHints kf stmt in widen wh s1 s2 diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml index ab4c24f45a6d23b5a03fe815b68502fb7bfd454c..93abea72d3e62b33148dbcc5ede6db82b730a992 100644 --- a/src/plugins/value/domains/printer_domain.ml +++ b/src/plugins/value/domains/printer_domain.ml @@ -34,6 +34,7 @@ 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 33bae1ed3a01b54fba5d06cbbfcb0fdf77549c77..721c68c5ea8361cca34195ed37865a89f2200335 100644 --- a/src/plugins/value/domains/simple_memory.ml +++ b/src/plugins/value/domains/simple_memory.ml @@ -47,7 +47,7 @@ module type S = sig val fold: (Base.t -> value -> 'a -> 'a) -> t -> 'a -> 'a end -module Make_Memory (Value: Value) = struct +module Make_Memory (Info: sig val name: string end) (Value: Value) = struct module Initial_Values = struct let v = [] end module Deps = struct let l = [Ast.self] end @@ -55,8 +55,10 @@ module Make_Memory (Value: Value) = struct include Hptmap.Make (Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps) + let name = Info.name + let cache_name s = - Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s) + Hptmap_sig.PersistentCache ("Value." ^ name ^ "." ^ s) let disjoint_union = let cache = cache_name "union" in @@ -186,7 +188,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct try Some (Hashtbl.find table name) with Not_found -> None - module M = Make_Memory (Value) + module M = Make_Memory (Info) (Value) include M include Domain_builder.Complete (M) diff --git a/src/plugins/value/domains/simple_memory.mli b/src/plugins/value/domains/simple_memory.mli index a194b4fe98797e8aa3438a4109d488bcf1cdb048..bbbd93735a956fa1ca8c9f9b9cb14a30a2d562b4 100644 --- a/src/plugins/value/domains/simple_memory.mli +++ b/src/plugins/value/domains/simple_memory.mli @@ -86,7 +86,7 @@ module type S = sig end (* Builds a memory from a value abstraction. *) -module Make_Memory (Value: Value) : sig +module Make_Memory (Info: sig val name: string end) (Value: Value) : sig include Datatype.S_with_collections include S with type t := t and type value := Value.t diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml index 0d95237c6476678c6147b3ece9ad12a34fda9616..a29ebf76b60a1ab71035a4ad56475fc377fa3925 100644 --- a/src/plugins/value/domains/symbolic_locs.ml +++ b/src/plugins/value/domains/symbolic_locs.ml @@ -182,7 +182,7 @@ module Memory = struct include Datatype.Serializable_undefined type t = memory - let name = "Value.Symbolic_locs.Memory.t" + let name = "symbolic-locations" let reprs = [ { values = List.hd K2V.M.reprs; zones = List.hd K2Z.reprs; diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml index 7d46ca1e8094212d0653b9db9d465f8deb6b053d..7cd38c393a807622d5c2d97166970f8959a5477e 100644 --- a/src/plugins/value/domains/taint_domain.ml +++ b/src/plugins/value/domains/taint_domain.ml @@ -75,7 +75,7 @@ module LatticeTaint = struct type t = taint - let name = "Value.Taint.t" + let name = "taint" let reprs = [ { locs_data = List.hd Zone.reprs; diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml index 52e14219be6b7f3d87404deb6e778f55890cc0a2..98cd954008c82b4b7f0fd80fbe920b5bbea07c5c 100644 --- a/src/plugins/value/domains/traces_domain.ml +++ b/src/plugins/value/domains/traces_domain.ml @@ -532,7 +532,7 @@ module Traces = struct include Datatype.Serializable_undefined type t = state - let name = "Value.Traces_domain.Traces.state" + let name = "traces" let reprs = [empty] diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml index 5307ef978d60d4ceeaf3a94501935175e8cfabc8..d7f7bb0a24495a638422370353bf576bbfee0e63 100644 --- a/src/plugins/value/domains/unit_domain.ml +++ b/src/plugins/value/domains/unit_domain.ml @@ -27,7 +27,7 @@ module Static = struct include Datatype.Unit type state = t - let name = "Unit domain" + let name = "unit" let log_category = log_key let structure = Abstract.Domain.Unit diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml index fedceb3f36ff2cd185349b8eb1b5f5303ce05829..c2221af95912657e3c1c5537a18c7ec5d8b94b5e 100644 --- a/src/plugins/value/engine/abstractions.ml +++ b/src/plugins/value/engine/abstractions.ml @@ -342,7 +342,6 @@ let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc (* 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 =