aboutsummaryrefslogtreecommitdiffstats
path: root/common/Sections.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-09 11:06:24 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-09 11:06:24 +0200
commit0ffd562ae1941e37471ac0c2b8f93bed1de26441 (patch)
tree2ac8382fa3a37568f32d27dbc3291c8cd97f13e2 /common/Sections.ml
parentf0a5038b4e4220300637d3e9e918d9ec31623108 (diff)
downloadcompcert-kvx-0ffd562ae1941e37471ac0c2b8f93bed1de26441.tar.gz
compcert-kvx-0ffd562ae1941e37471ac0c2b8f93bed1de26441.zip
Filled in the rest of the funciton needed for thte debug info under arm.
The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass.
Diffstat (limited to 'common/Sections.ml')
-rw-r--r--common/Sections.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/common/Sections.ml b/common/Sections.ml
index be0f415e..cc8b0758 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -30,6 +30,7 @@ type section_name =
| Section_debug_info of string
| Section_debug_abbrev
| Section_debug_loc
+ | Section_debug_line of string
type access_mode =
| Access_default