diff options
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Cprint.ml | 6 | ||||
-rw-r--r-- | cparser/Cprint.mli | 1 | ||||
-rw-r--r-- | cparser/Elab.ml | 2 | ||||
-rw-r--r-- | cparser/Unblock.ml | 20 |
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 } |