diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-20 15:36:42 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-20 15:36:42 +0200 |
| commit | a34b64ee2e7a535ebc0fc731243ab520c4ba430f (patch) | |
| tree | 21404821c5554252ceafb95d8b9573b218664eab /cparser | |
| parent | 31aceeb1be64d529432f35bbea16ebafc3a21df0 (diff) | |
| download | compcert-a34b64ee2e7a535ebc0fc731243ab520c4ba430f.tar.gz compcert-a34b64ee2e7a535ebc0fc731243ab520c4ba430f.zip | |
New version of adding scopes etc.
Instead of reimplementing the whole scope handling in the debug information
use the existing functionality and fill the scopes explicitly in the functions.
Diffstat (limited to 'cparser')
| -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 6c941a1f..e802085d 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 sto id ty loc; + Debug.insert_local_declaration (-1) sto id ty loc;(* Dummy scope *) {sdesc = Sdecl d; sloc = loc}) dcl @ elab_block_body env' ctx sl1 | s :: sl1 -> |