Record the scope structure during unblocking.

Instead of creating separate annotations for the local variables
we call the Debug.add_lvar_scope and we construct a mapping from
function id + scope id to scope information.

4 files changed, 18 insertions, 11 deletions

diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 4ceaa016..1af5af1e 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -20,6 +20,8 @@ open C
 
 let print_idents_in_full = ref false
 
+let print_debug_idents = ref false
+
 let print_line_numbers = ref false
 
 let location pp (file, lineno) =
@@ -27,7 +29,9 @@ let location pp (file, lineno) =
     fprintf pp "# %d \"%s\"@ " lineno file
 
 let ident pp i =
-  if !print_idents_in_full
+  if !print_debug_idents
+  then fprintf pp "$%d" i.stamp
+  else if !print_idents_in_full
   then fprintf pp "%s$%d" i.name i.stamp
   else fprintf pp "%s" i.name
 
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index d63e341c..349b5f9a 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -15,6 +15,7 @@
 
 val print_idents_in_full : bool ref
 val print_line_numbers : bool ref
+val print_debug_idents : bool ref
 
 val location : Format.formatter -> C.location -> unit
 val attributes : Format.formatter -> C.attributes -> unit
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 021dc512..33c4822d 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2227,7 +2227,7 @@ and elab_block_body env ctx sl =
       let (dcl, env') = elab_definition true env def in
       let loc = elab_loc (get_definitionloc def) in
       List.map (fun ((sto,id,ty,_) as d) ->
-        Debug.insert_local_declaration (-1) sto id ty loc;(* Dummy scope *)
+        Debug.insert_local_declaration sto id ty loc;
         {sdesc = Sdecl d; sloc = loc}) dcl
       @ elab_block_body env' ctx sl1
   | s :: sl1 ->
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index b5f945d4..4f5056bb 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -217,8 +217,11 @@ let add_lineno ctx prev_loc this_loc s =
 (* Variable declaration annotation:
       __builtin_debug(6, var, scope)  *)
 
+let curr_fun_id = ref 0
+
 let debug_var_decl ctx id ty =
   let scope = match ctx with [] -> 0 | sc :: _ -> sc in
+  Debug.add_lvar_scope !curr_fun_id id scope;
   debug_annot 6L
     [ {edesc = EVar id; etyp = ty}; integer_const scope ]
 
@@ -227,13 +230,6 @@ let add_var_decl ctx id ty s =
   then sseq no_loc (debug_var_decl ctx id ty) s
   else s
 
-let add_param_decls params body =
-  if !Clflags.option_g then
-    List.fold_right
-      (fun (id, ty) s -> sseq no_loc (debug_var_decl [] id ty) s)
-      params body
-  else body
-
 (* Generate fresh scope identifiers, for blocks that contain at least
    one declaration *)
 
@@ -313,7 +309,10 @@ let rec unblock_stmt env ctx ploc s =
   | Sblock sl ->
       let ctx' =
         if block_contains_decl sl
-        then new_scope_id () :: ctx
+        then
+          let id = new_scope_id () in
+          Debug.enter_scope !curr_fun_id (List.hd ctx) id;
+          id:: ctx
         else ctx in
       unblock_block env ctx' ploc sl
   | Sdecl d ->
@@ -342,8 +341,11 @@ and unblock_block env ctx ploc = function
 let unblock_fundef env f =
   local_variables := [];
   next_scope_id := 0;
+  curr_fun_id := f.fd_name.stamp;
+  let id = new_scope_id () in
+  Debug.enter_function_scope f.fd_name id;
   let body =
-    add_param_decls f.fd_params (unblock_stmt env [] no_loc f.fd_body) in
+    (unblock_stmt env [id] no_loc f.fd_body) in
   let decls = !local_variables in
   local_variables := [];
   { f with fd_locals = f.fd_locals @ decls; fd_body = body }