aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/TargetPrinter.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 19:49:56 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 19:49:56 +0100
commit424df9761ae4f3c9ce91ba785aef111bedd9125a (patch)
treebf140016b5fcd6b5d1131b23c88e7c331b70d949 /riscV/TargetPrinter.ml
parentf69ba5f0bb0ee5e2b08f57290bee9635dd13f33c (diff)
downloadcompcert-kvx-424df9761ae4f3c9ce91ba785aef111bedd9125a.tar.gz
compcert-kvx-424df9761ae4f3c9ce91ba785aef111bedd9125a.zip
fixes for aarch64 arm ppc ppc64
Diffstat (limited to 'riscV/TargetPrinter.ml')
-rw-r--r--riscV/TargetPrinter.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 64bcea4c..1f02ca71 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -107,7 +107,9 @@ module Target : TARGET =
let name_of_section = function
| Section_text -> ".text"
- | Section_data i | Section_small_data i ->
+ | 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 ()
| Section_const i | Section_small_const i ->
if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM"