diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
| commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
| tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /kvx/TargetPrinter.ml | |
| parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
| parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
| download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip | |
Merge branch 'master' into merge_master_8.13.1
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
Diffstat (limited to 'kvx/TargetPrinter.ml')
| -rw-r--r-- | kvx/TargetPrinter.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml index 5b6230ca..9e2e3776 100644 --- a/kvx/TargetPrinter.ml +++ b/kvx/TargetPrinter.ml @@ -201,14 +201,16 @@ module Target (*: TARGET*) = let name_of_section = function | Section_text -> ".text" - | Section_data(true, true) -> + | Section_data(Init, true) -> ".section .tdata,\"awT\",@progbits" - | Section_data(false, true) -> + | Section_data(Uninit, true) -> ".section .tbss,\"awT\",@nobits" + | Section_data(Init_reloc, true) -> + failwith "Sylvain does not how to fix this" | Section_data(i, false) | Section_small_data(i) -> - (if i then ".data" else "COMM") + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata" | Section_jumptable -> ".section .rodata" |