diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-21 14:45:28 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-21 14:45:28 +0200 |
| commit | d8aac95c8d1767bf3b10990599b0f32687994182 (patch) | |
| tree | 1d883ab45812c372b6651423b43b9fd67b77e2fb /backend/PrintAsmaux.ml | |
| parent | 9147350fdb47f3471ce6d9202b7c996f79ffab2d (diff) | |
| download | compcert-kvx-d8aac95c8d1767bf3b10990599b0f32687994182.tar.gz compcert-kvx-d8aac95c8d1767bf3b10990599b0f32687994182.zip | |
Continuing experiment: track the scopes of local variables via __builtin_debug
As observed by B. Schommer, it is not enough to track scopes for every source line, as blocks can occur on a single line (think macros). Hence:
- Revert debug annotations of kind 1 to contain only line number info.
Generate them only when the line number changes.
- Use debug annotations of kind 6 to record the list of active scopes
(as BA_int integer arguments to __builtin_annot). Generate them
before every nontrivial statement, even if on the same line as others.
- Remove the generation of "variable x is declared in scope N" debug
annotations. This can be tracked separately and more efficiently.
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 13daa644..a67c85d2 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -269,8 +269,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)) @@ -285,9 +283,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; | _ -> () |