From 0905e812698104cf16aacb575e1afaa3a8c33bd0 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 22 Mar 2021 14:55:26 +0100
Subject: [PATCH] [Eva] Register message key to enable debug printing.
---
src/plugins/value/domains/taint_domain.ml | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index a628704d946..5324e1b50c4 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -38,9 +38,11 @@ type taint = {
assume_stmts: Stmt.Set.t;
}
-(* Set to true for pretty-printing also [assume_stmts] on
+let dkey = Value_parameters.register_category "d-taint"
+
+(* Debug key to also include [assume_stmts] in the output of the
Frama_C_domain_show_each directive. *)
-let debug = false
+let dkey_debug = Value_parameters.register_category "d-taint-debug"
module LatticeTaint = struct
@@ -90,7 +92,7 @@ module LatticeTaint = struct
let equal = Datatype.from_compare
let pretty fmt t =
- if debug
+ if Value_parameters.is_debug_key_enabled dkey_debug
then pp_state fmt t
else pp_locs_only fmt t
@@ -340,7 +342,7 @@ module InternalTaint = struct
include (ReuseTaint: Abstract_domain.Reuse with type t := state)
let name = "taint"
- let log_category = Value_parameters.register_category "d-taint"
+ let log_category = dkey
(* Logic. *)
--
GitLab