diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-04 16:03:14 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-04 16:03:14 +0100 |
| commit | afbf8601af31b012872a2fae6939be9fd231145f (patch) | |
| tree | 45cd9a15d089a32e2f92a821f04acacbc4c76558 /backend/CSE3analysisaux.ml | |
| parent | decb2ce78a04fe4432aead78ca0165106fd4d26d (diff) | |
| download | compcert-kvx-afbf8601af31b012872a2fae6939be9fd231145f.tar.gz compcert-kvx-afbf8601af31b012872a2fae6939be9fd231145f.zip | |
do not print "refining" unless asked
Diffstat (limited to 'backend/CSE3analysisaux.ml')
| -rw-r--r-- | backend/CSE3analysisaux.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index bd4ca20a..e37ef61f 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); |