diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-08-22 17:35:49 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-08-29 13:55:35 +0200 |
| commit | 169007c52e27ce1fce6ca5fdd5fc7f43071b8841 (patch) | |
| tree | 86e52680d32759cf4c78219fb245bd0467c070a1 /common/Sections.mli | |
| parent | 50836f2a04575402aa61a256fe7047c16610992f (diff) | |
| download | compcert-169007c52e27ce1fce6ca5fdd5fc7f43071b8841.tar.gz compcert-169007c52e27ce1fce6ca5fdd5fc7f43071b8841.zip | |
Support mergeable sections for fixed-size literals
On platforms that support them (ELF, macOS), use mergeable sections
(like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals.
Works only if the LITERAL section is the default one. If the user
provided their own LITERAL section, all literals are put in it
regardless of their sizes.
Support for mergeable string sections is introduced in this commit too
but needs further changes in C2C.ml .
Diffstat (limited to 'common/Sections.mli')
| -rw-r--r-- | common/Sections.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/common/Sections.mli b/common/Sections.mli index 8ec98e40..33fdeab8 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -28,8 +28,8 @@ type section_name = | Section_small_data of initialized | Section_const of initialized | Section_small_const of initialized - | Section_string - | Section_literal + | Section_string of int (* character size; zero if unknown *) + | Section_literal of int (* literal size; zero if unknown *) | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) | Section_debug_abbrev @@ -55,4 +55,5 @@ val use_section_for: AST.ident -> string -> bool val for_variable: Env.t -> C.location -> AST.ident -> C.typ -> initialized -> section_name * access_mode val for_function: Env.t -> C.location -> AST.ident -> C.attributes -> section_name list -val for_stringlit: unit -> section_name +val for_stringlit: int -> section_name +val with_size: int -> section_name -> section_name |