diff options
author | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-20 08:18:42 +0000 |
---|---|---|
committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-20 08:18:42 +0000 |
commit | 2829523d71dfe92c1adc9cf59851639e895ae996 (patch) | |
tree | a3ef12df2dafd6c74d1fe66b7e8aace1cae4265c /checklink/Frameworks.ml | |
parent | 3f205ff4314ccac92e4d74951929aa31b0308274 (diff) | |
download | compcert-kvx-2829523d71dfe92c1adc9cf59851639e895ae996.tar.gz compcert-kvx-2829523d71dfe92c1adc9cf59851639e895ae996.zip |
Added small data area support to checklink
Accesses to small data areas are dynamically resolved by constructing a
mapping from registers to virtual addresses they are supposed to point
to. This mapping is reported.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1880 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Frameworks.ml')
-rw-r--r-- | checklink/Frameworks.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index 4054b681..4e987350 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -38,7 +38,13 @@ type e_framework = { chkd_bytes_list: (int32 * int32 * int * byte_chunk_desc) list; chkd_fun_syms: bool array; chkd_data_syms: bool array; + (** The mapping from CompCert sections to ELF sections will be inferred along + the way. This way, we can check things without prior knowledge of the + linker script. *) section_map: string StringMap.t; + (** We will assign a virtual address to each register that can act as an SDA + base register. *) + sda_map: int32 IntMap.t; } module PosOT = struct @@ -110,6 +116,11 @@ let section_map = { set = (fun m ef -> { ef with section_map = m }); } +let sda_map = { + get = (fun ef -> ef.sda_map); + set = (fun m ef -> { ef with sda_map = m }); +} + let ident_to_sym_ndx = { get = (fun sf -> sf.ident_to_sym_ndx); set = (fun i sf -> { sf with ident_to_sym_ndx = i }); |