From afbf8601af31b012872a2fae6939be9fd231145f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 4 Nov 2020 16:03:14 +0100
Subject: [PATCH] do not print "refining" unless asked
---
backend/CSE3analysisaux.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index bd4ca20af..e37ef61f3 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -139,7 +139,8 @@ let refine_invariants
if not (RB.beq cur nxt)
then
begin
- Printf.printf "refining CSE3 node %d\n" (P.to_int pc);
+ (if !Clflags.option_debug_compcert > 4
+ then Printf.printf "refining CSE3 node %d\n" (P.to_int pc));
List.iter add_todo (successors pc)
end in
(List.iter add_todo nodes);
--
GitLab