diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-22 19:44:47 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-22 19:44:47 +0200 |
| commit | d7f75509c290d871cb8cd8aa11a0be2923c9ef17 (patch) | |
| tree | 5e1cfd9366ae875a5da7286d1912b7fab7454ce0 /cparser/Elab.ml | |
| parent | 4b9b0e8f988cdfa1f848919b41bfe24c6e9a052a (diff) | |
| download | compcert-d7f75509c290d871cb8cd8aa11a0be2923c9ef17.tar.gz compcert-d7f75509c290d871cb8cd8aa11a0be2923c9ef17.zip | |
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.
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |