aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DebugInformation.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-30 15:39:26 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-30 15:39:26 +0200
commit4421b4168ad82d326665662a1a56a4db3cd41a11 (patch)
tree6f082989f45ab497d3116d91f2c381d27b8224ec /debug/DebugInformation.ml
parentefd2afc1c11ba2e6f46b25a028b5c1c56f0bc2c1 (diff)
downloadcompcert-kvx-4421b4168ad82d326665662a1a56a4db3cd41a11.tar.gz
compcert-kvx-4421b4168ad82d326665662a1a56a4db3cd41a11.zip
More robust dwarf generation. Do not add incomplete local variables
in the Debuging information.
Diffstat (limited to 'debug/DebugInformation.ml')
-rw-r--r--debug/DebugInformation.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 382845a4..0249f20b 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -665,7 +665,7 @@ let insert_local_declaration sto id ty loc =
lvar_file_loc = loc;
lvar_type = ty;
lvar_static = sto = Storage_static;
- } in
+ } in
let id' = next_id () in
Hashtbl.add local_variables id' (LocalVariable var);
Hashtbl.add stamp_to_local id.stamp id'