diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-23 11:13:27 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-23 11:13:27 +0200 |
| commit | 806102dd5492a39b33c2ebb88d6646237ba7f9e6 (patch) | |
| tree | 8960777f82ef21dcf269d68b914ae37308339f60 /backend/PrintAsmaux.ml | |
| parent | d7f75509c290d871cb8cd8aa11a0be2923c9ef17 (diff) | |
| parent | d8aac95c8d1767bf3b10990599b0f32687994182 (diff) | |
| download | compcert-kvx-806102dd5492a39b33c2ebb88d6646237ba7f9e6.tar.gz compcert-kvx-806102dd5492a39b33c2ebb88d6646237ba7f9e6.zip | |
Merge branch 'debugscopes' into debug_locations
Conflicts:
cparser/Unblock.ml
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index a0474003..3f0b3ea3 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -267,8 +267,6 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = args in match kind with | 1 -> (* line number *) - fprintf oc "%s debug: current scopes%a\n" - comment print_debug_args args; if Str.string_match re_file_line txt 0 then print_line oc (Str.matched_group 1 txt) (int_of_string (Str.matched_group 2 txt)) @@ -283,9 +281,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = | 5 -> (* local variable preallocated in stack *) fprintf oc "%s debug: %s resides at%a\n" comment txt print_debug_args args - | 6 -> (* declaration of a local variable *) - fprintf oc "%s debug: %s declared in scope%a\n" - comment txt print_debug_args args + | 6 -> (* scope annotations *) + fprintf oc "%s debug: current scopes%a\n" + comment print_debug_args args; | _ -> () |