From 5a5d16abc786834f5e4f1bfe6412a17900c22ef5 Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 4 Apr 2012 11:59:41 +0000
Subject: Tracing each data chunk in debug mode

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1873 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Check.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'checklink/Check.ml')

diff --git a/checklink/Check.ml b/checklink/Check.ml
index be56fe0..3559980 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -2413,6 +2413,13 @@ let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framewor
     match l with
     | [] -> OK(sfw, s)
     | d::l ->
+        let sfw =
+          if !debug
+          then (
+            (sf_ef ^%= add_log (DEBUG(string_of_init_data d))) sfw
+          )
+          else sfw
+        in
         begin match d with
         | Init_int8(i) -> (
           bitmatch bs with
-- 
cgit v1.2.3