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

1 files changed, 11 insertions, 0 deletions

diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 4054b68..4e98735 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 });