Merge remote-tracking branch 'origin/master' into named-externals

Conflicts:
	arm/TargetPrinter.ml
	backend/CMparser.mly
	backend/SelectLongproof.v
	backend/Selectionproof.v
	cfrontend/C2C.ml
	checklink/Asm_printers.ml
	checklink/Check.ml
	checklink/Fuzz.ml
	common/AST.v
	debug/DebugInformation.ml
	debug/DebugInit.ml
	debug/DwarfPrinter.ml
	debug/DwarfTypes.mli
	debug/Dwarfgen.ml
	exportclight/ExportClight.ml
	ia32/TargetPrinter.ml
	powerpc/Asm.v
	powerpc/SelectOpproof.v
	powerpc/TargetPrinter.ml

1 files changed, 3 insertions, 8 deletions

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index a938725a..9f2c66cf 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -157,7 +157,8 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Section_debug_loc -> ".section	.debug_loc,\"\",%progbits"
       | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",%progbits"
       | Section_debug_line _ -> ".section	.debug_line,\"\",%progbits"
-
+      | Section_debug_ranges -> ".section	.debug_ranges,\"\",%progbits"
+      | Section_debug_str -> ".section	.debug_str,\"MS\",%progbits,1"
 
     let section oc sec =
       fprintf oc "	%s\n" (name_of_section sec)
@@ -901,21 +902,15 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       fprintf oc "	.%s\n" (if !Clflags.option_mthumb then "thumb" else "arm");
       if !Clflags.option_g then begin
         section oc Section_text;
-        let low_pc = new_label () in
-        Debug.add_compilation_section_start ".text" low_pc;
-        fprintf oc "%a:\n" elf_label low_pc;
         fprintf oc "	.cfi_sections	.debug_frame\n"
       end
 
 
     let print_epilogue oc =
       if !Clflags.option_g then begin
-        let high_pc = new_label () in
-        Debug.add_compilation_section_end ".text" high_pc;
         Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
         section oc Section_text;
-        fprintf oc "%a:\n" elf_label high_pc
-        end
+      end
 
 
     let default_falignment = 4