diff options
| author |  varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-04 11:59:41 +0000 |
|---|---|---|
| committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-04 11:59:41 +0000 |
| commit | 5a5d16abc786834f5e4f1bfe6412a17900c22ef5 (patch) | |
| tree | 40c9d5ac1a62a568edeb782a5a3804699078b357 /checklink | |
| parent | 32a6fcb12814550633261960b540ffeb8a0fcab5 (diff) | |
Tracing each data chunk in debug mode
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1873 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Asm_printers.ml | 9 | ||||
| -rw-r--r-- | checklink/Check.ml | 7 |
2 files changed, 16 insertions, 0 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 8f78a07..9f6a540 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -228,3 +228,12 @@ let string_of_instruction = function | Pbuiltin (e0, p1, p2) -> "Pbuiltin(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_preg ", " p1 ^ ", " ^ string_of_preg p2 ^ ")" | Pannot (e0, a1) -> "Pannot(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_annot_param ", " a1 ^ ")" +let string_of_init_data = function +| Init_int8(i) -> "Init_int8(" ^ string_of_int (z_int_lax i) ^ ")" +| Init_int16(i) -> "Init_int16(" ^ string_of_int (z_int_lax i) ^ ")" +| Init_int32(i) -> "Init_int32(" ^ string_of_int32i (z_int32 i) ^ ")" +| Init_float32(f) -> "Init_float32(" ^ string_of_float f ^ ")" +| Init_float64(f) -> "Init_float64(" ^ string_of_float f ^ ")" +| Init_space(z) -> "Init_space(" ^ string_of_int (z_int z) ^ ")" +| Init_addrof(ident, ofs) -> + "Init_addrof(" ^ string_of_pos ident ^ ", " ^ string_of_int32i (z_int32 ofs) ^ ")" 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 |