diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-17 18:19:37 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-17 18:19:37 +0200 |
| commit | c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93 (patch) | |
| tree | c9dacff414156d4d527ac40078cbdc51f160c8d0 /cparser/Elab.ml | |
| parent | 98cddc7ba45b34fbd71d9a80c27a8e5ec6b311b0 (diff) | |
| download | compcert-c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93.tar.gz compcert-c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93.zip | |
First version with computation of dwarf info from debug info.
Introduced a new dwarf generation from the information collected in
the DebugInformation and removed the old CtODwarf translation.
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index ca5865dd..6839ac9f 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -56,10 +56,10 @@ let elab_loc l = (l.filename, l.lineno) let top_declarations = ref ([] : globdecl list) -let emit_elab env loc td = +let emit_elab ?(enter:bool=true) env loc td = let loc = elab_loc loc in let dec ={ gdesc = td; gloc = loc } in - Debug.insert_global_declaration env dec; + if enter then Debug.insert_global_declaration env dec; top_declarations := dec :: !top_declarations let reset() = top_declarations := [] @@ -1901,7 +1901,7 @@ let elab_fundef env spec name body loc = let (func_ty, func_init) = __func__type_and_init s in let (func_id, _, env3,func_ty) = enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in - emit_elab env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); + emit_elab ~enter:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body' = !elab_funbody_f ty_ret env3 body in (* Special treatment of the "main" function *) |