aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-11-10 17:39:02 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-11-10 17:39:02 +0100
commit8c1b59808e9ee9888a846de2e3ff111628863f28 (patch)
tree31e0a043e6b437170d3ed84df8473a9599c27a4c
parent35e3f39bf967c4ed2ba3390b488604554306065d (diff)
downloadcompcert-kvx-8c1b59808e9ee9888a846de2e3ff111628863f28.tar.gz
compcert-kvx-8c1b59808e9ee9888a846de2e3ff111628863f28.zip
Do not enforce locations for function parameters.
In the case of struct function parameters it is not always guaranteed that they are still there and not translated into plain integer arguments. Bug 17609.
-rw-r--r--debug/Dwarfgen.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index f62fac26..7addaba3 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -384,7 +384,9 @@ module Dwarfgenaux (Target: TARGET) =
with Not_found -> None,[]
let function_parameter_to_entry f_id acc p =
- let loc,loc_list = location_entry f_id (get_opt_val p.parameter_atom) in
+ let loc,loc_list = match p.parameter_atom with
+ | None -> None,[]
+ | Some p -> location_entry f_id p in
let p = {
formal_parameter_artificial = None;
formal_parameter_name = name_opt p.parameter_name;