aboutsummaryrefslogtreecommitdiffstats
path: root/arm/TargetPrinter.ml
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-06-11 11:41:37 +0200
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2021-06-11 11:41:37 +0200
commitaf16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch)
tree4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /arm/TargetPrinter.ml
parent21c979fce33b068ce4b86e67d3d866b203411c6c (diff)
parent02b169b444c435b8d1aacf54969dd7de57317a5c (diff)
downloadcompcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz
compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'arm/TargetPrinter.ml')
-rw-r--r--arm/TargetPrinter.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 839530c6..9269dd29 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -150,9 +150,9 @@ struct
| Section_data(i, true) ->
failwith "_Thread_local unsupported on this platform"
| Section_data(i, false) | Section_small_data(i) ->
- if i then ".data" else common_section ()
+ variable_section ~sec:".data" ~bss:".bss" i
| Section_const i | Section_small_const i ->
- if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM"
+ variable_section ~sec:".section .rodata" i
| Section_string -> ".section .rodata"
| Section_literal -> ".text"
| Section_jumptable -> ".text"