New section mapping checks and symbol data lookup

Section mapping is now discovered on-the-fly, and linker script remappings
are reported as warnings at the end. Symbol data lookup is now able to
gracefully fail if the symbol's virtual address is not within the range of
its parent section's virtual address space.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1878 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 6 insertions, 0 deletions

diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index f35672d..4054b68 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -38,6 +38,7 @@ type e_framework = {
   chkd_bytes_list: (int32 * int32 * int * byte_chunk_desc) list;
   chkd_fun_syms: bool array;
   chkd_data_syms: bool array;
+  section_map: string StringMap.t;
 }
 
 module PosOT = struct
@@ -104,6 +105,11 @@ let log = {
   set = (fun l ef -> { ef with log = l });
 }
 
+let section_map = {
+  get = (fun ef -> ef.section_map);
+  set = (fun m ef -> { ef with section_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 });