diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-18 16:42:05 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-18 16:42:05 +0200 |
| commit | 31aceeb1be64d529432f35bbea16ebafc3a21df0 (patch) | |
| tree | acb6e197e6960405b450c9c9842fdf37e18a5b40 /cparser | |
| parent | c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93 (diff) | |
| download | compcert-31aceeb1be64d529432f35bbea16ebafc3a21df0.tar.gz compcert-31aceeb1be64d529432f35bbea16ebafc3a21df0.zip | |
Started implementing the scope for the Debug Informations.
Scopes will be handled by a stack of all open scopes. This stack
then can also be used to generate the debug directives to track the
scopes through the rest of the passes.
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 6839ac9f..6c941a1f 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2226,7 +2226,9 @@ and elab_block_body env ctx sl = | DEFINITION def :: sl1 -> let (dcl, env') = elab_definition true env def in let loc = elab_loc (get_definitionloc def) in - List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl + List.map (fun ((sto,id,ty,_) as d) -> + Debug.insert_local_declaration sto id ty loc; + {sdesc = Sdecl d; sloc = loc}) dcl @ elab_block_body env' ctx sl1 | s :: sl1 -> let s' = elab_stmt env ctx s in |