aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-08-15 09:18:25 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-08-15 09:18:25 +0200
commitc9f8b8e598808775bf4e5072aa47c94625677f7c (patch)
tree297a41ea9b8a2e2f08aa451c06ed7c66659c650c
parent0eefd517c797f2f17ef9228e5a4d07c5dc8ecada (diff)
downloadcompcert-c9f8b8e598808775bf4e5072aa47c94625677f7c.tar.gz
compcert-c9f8b8e598808775bf4e5072aa47c94625677f7c.zip
Do not use `.rodata.cst8` for floating-point literals
FP literals can have size 4 or 8 bytes, and it's incorrect to put a 4-byte literal in a mergeable section of chunk size 8. Fixes: #447
-rw-r--r--powerpc/TargetPrinter.ml2
-rw-r--r--x86/TargetPrinter.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 52d30e33..5c414b56 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -129,7 +129,7 @@ module Linux_System : SYSTEM =
| Section_small_const i ->
variable_section ~sec:".section .sdata2,\"a\",@progbits" i
| Section_string -> ".rodata"
- | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8"
+ | Section_literal -> ".section .rodata"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\",\"a%s%s\",@progbits"
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 5bc2be1c..65e44f7d 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -139,7 +139,7 @@ module ELF_System : SYSTEM =
| Section_const i | Section_small_const i ->
variable_section ~sec:".section .rodata" i
| Section_string -> ".section .rodata"
- | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8"
+ | Section_literal -> ".section .rodata"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\",\"a%s%s\",@progbits"