[Eva] Adds help to Eva message category.

src/plugins/eva/domains/cvalue/builtins_malloc.ml

@@ -27,6 +27,7 @@ open Cvalue
 open Lattice_bounds
 
 let dkey = Self.register_category "malloc"
+    ~help:"messages from the builtins interpreting dynamic allocations"
 
 let wkey_weak_alloc = Self.register_warn_category "malloc:weak"
 let () = Self.set_warn_status wkey_weak_alloc Log.Winactive

src/plugins/eva/domains/cvalue/builtins_memory.ml

@@ -30,6 +30,8 @@ let register_builtin name ?replace builtin =
   Builtins.register_builtin name ?replace Cacheable builtin
 
 let dkey = Self.register_category "imprecision"
+    ~help:"messages related to possible imprecision of builtins interpreting \
+           memcpy, memmove and memset"
 
 let rec pretty_lval_of_address exp =
   match exp.node with

src/plugins/eva/domains/cvalue/cvalue_domain.ml

@@ -23,6 +23,8 @@
 open Eval
 
 let dkey_card = Self.register_category "cardinal"
+    ~help:"estimate the number of concrete states approximated by the analysis \
+           at the end of each function"
 
 module State = struct
 

src/plugins/eva/domains/cvalue/cvalue_init.ml

@@ -25,8 +25,6 @@
 open Cil_types
 open Locations
 
-let dkey = Self.register_category "initial-state"
-
 let add_initialized state loc v =
   Cvalue.Model.add_binding ~exact:true state loc v
 
@@ -86,8 +84,9 @@ let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
        | UnknownValidity -> Base.Unknown (a, None, b)
       )
     | Base.Unknown _ -> (* Unknown validity is caused by strange type *)
-      Self.result ~dkey "creating variable %s with imprecise \
-                         size (type %a)" hidden_var_name Printer.pp_typ pointed_typ;
+      Self.result ~dkey:Self.dkey_initial_state
+        "creating variable %s with imprecise size (type %a)"
+        hidden_var_name Printer.pp_typ pointed_typ;
       validity
     | Base.Empty | Base.Known _ | Base.Invalid -> validity
     | Base.Variable _ -> (* should never happen (validity_from_type cannot

src/plugins/eva/domains/domain_builder.ml

@@ -99,7 +99,12 @@ module Complete (Domain: InputDomain) = struct
 
   module Store = Domain_store.Make (Domain)
 
-  let log_category = Self.register_category ("d-" ^ Domain.name)
+  let log_category =
+    let help =
+      Format.asprintf
+        "print states of the %s domain on some user directives" Domain.name
+    in
+    Self.register_category ("d-" ^ Domain.name) ~help
 
   let key: Domain.t Structure.Key_Domain.key =
     Structure.Key_Domain.create_key Domain.name

src/plugins/eva/domains/domain_product.ml

@@ -24,7 +24,8 @@ open Eval
 
 let counter = ref 0
 
-let product_category = Self.register_category "domain_product"
+let product_category =
+  Self.register_category "domain_product" ~help:"inactive category"
 
 module Make
     (Context  : Abstract_context.S)

src/plugins/eva/domains/taint_domain.ml

@@ -44,6 +44,7 @@ type taint_state = {
 (* Debug key to also include [assume_stmts] in the output of the
    Frama_C_domain_show_each directive. *)
 let dkey_debug = Self.register_category "d-taint-debug"
+    ~help:"debug print of the taint domain"
 
 let wkey = Self.register_warn_category "taint"
 

src/plugins/eva/engine/subdivided_evaluation.ml

@@ -23,6 +23,7 @@
 open Eval
 
 let dkey = Self.register_category "nonlin"
+    ~help:"messages about evaluation of subdivisions enabled by -eva-subdivide-non-linear"
 
 (* ----------------- Occurrences of lvalues in expressions ------------------ *)
 

src/plugins/eva/self.ml

@@ -75,14 +75,41 @@ let is_computed () =
   | NotComputed | Computing -> false
 
 (* Debug categories. *)
-let dkey_initial_state = register_category "initial-state"
-let dkey_final_states = register_category "final-states"
-let dkey_summary = register_category "summary"
-let dkey_pointer_comparison = register_category "pointer-comparison"
-let dkey_cvalue_domain = register_category "d-cvalue"
-let dkey_iterator = register_category "iterator"
-let dkey_widening = register_category "widening"
-let dkey_recursion = register_category "recursion"
+let dkey_initial_state =
+  register_category "initial-state"
+    ~help:"at the start of the analysis, \
+           print the initial value of global variables"
+
+let dkey_final_states =
+  register_category "final-states"
+    ~help:"at the end of the analysis, print final values inferred \
+           at the return point of each analyzed function "
+
+let dkey_summary =
+  register_category "summary"
+    ~help:"print a summary of the analysis at the end, including coverage \
+           and alarm numbers"
+
+let dkey_pointer_comparison =
+  register_category "pointer-comparison"
+    ~help:"messages about the evaluation of pointer comparisons"
+
+let dkey_cvalue_domain =
+  register_category "d-cvalue"
+    ~help:"print states of the cvalue domain on some user directives"
+
+let dkey_iterator =
+  register_category "iterator"
+    ~help:"debug messages about the fixpoint engine on the control-flow graph \
+           of functions"
+
+let dkey_widening =
+  register_category "widening"
+    ~help:"print a message at each point where the analysis applies a widening"
+
+let dkey_recursion =
+  register_category "recursion"
+    ~help:"print a message for each recursive call"
 
 let () =
   let activate dkey = add_debug_keys dkey in

src/plugins/eva/types/callstack.ml

@@ -23,6 +23,7 @@
 let stable_hash x = Hashtbl.seeded_hash 0 x
 
 let dkey_callstack = Self.register_category "callstack"
+    ~help:"additionally print the current callstack in some messages"
 
 module Thread = Int (* Threads are identified by integers *)
 module Kf = Kernel_function

src/plugins/eva/utils/widen_hints_ext.ml

@@ -23,6 +23,7 @@
 open Cil_types
 
 let dkey = Self.register_category "widen-hints"
+    ~help:"debug messages when failing to use widen_hints annotations"
 
 let error ?msg loc typing_context =
   typing_context.Logic_typing.error loc