aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-03-20 11:11:24 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-03-20 11:11:24 +0100
commit5bfa0059a144fb4333bbfecaa74690ba92a879ce (patch)
treef79baab2043f0d4f9687a20d2afe51853f13acc7 /debug
parenta968152051941a0fc50a86c3fc15e90e22ed7c47 (diff)
downloadcompcert-5bfa0059a144fb4333bbfecaa74690ba92a879ce.tar.gz
compcert-5bfa0059a144fb4333bbfecaa74690ba92a879ce.zip
Quote directory for comp_dir entry.
The compilation directory entry needs quoting since it could be a toplevel directory under windows. Bug 21216
Diffstat (limited to 'debug')
-rw-r--r--debug/Dwarfgen.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index ee568042..ca5d783d 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -549,7 +549,7 @@ let diab_gen_compilation_section s defs acc =
let cp = {
compile_unit_name = Simple_string !file_name;
compile_unit_range = Pc_pair (low_pc,high_pc);
- compile_unit_dir = Simple_string (Sys.getcwd ());
+ compile_unit_dir = Simple_string (Filename.quote (Sys.getcwd ()));
compile_unit_prod_name = Simple_string prod_name
} in
let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
@@ -620,7 +620,7 @@ let gen_gnu_debug_info sec_name var_section : debug_entries =
let cp = {
compile_unit_name = gnu_string_entry !file_name;
compile_unit_range = r;
- compile_unit_dir = gnu_string_entry (Sys.getcwd ());
+ compile_unit_dir = gnu_string_entry (Filename.quote (Sys.getcwd ()));
compile_unit_prod_name = gnu_string_entry prod_name;
} in
let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in