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, 14 insertions, 9 deletions

diff --git a/checklink/PPC_utils.ml b/checklink/PPC_utils.ml
index d027649..338c4c5 100644
--- a/checklink/PPC_utils.ml
+++ b/checklink/PPC_utils.ml
@@ -5,28 +5,33 @@ open PPC_parsers
 open PPC_types
 
 let code_at_vaddr (e: elf) (vaddr: int32) (nb_instr: int): ecode option =
-  match section_at_vaddr e vaddr with
+  begin match section_at_vaddr e vaddr with
   | None -> None
   | Some(sndx) ->
-      let code_bs =
-        bitstring_at_vaddr e sndx vaddr (32 * nb_instr) in
-      Some (parse_code_as_list code_bs)
+      begin match bitstring_at_vaddr e sndx vaddr (32 * nb_instr) with
+      | None -> None
+      | Some(code_bs) -> Some (parse_code_as_list code_bs)
+      end
+  end
 
 let code_of_sym_ndx (e: elf) (ndx: int): ecode option =
   let sym = e.e_symtab.(ndx) in
-  match sym.st_type with
+  begin match sym.st_type with
   | STT_FUNC ->
       let sym_vaddr = sym.st_value in
       let sym_size = Safe.(of_int32 sym.st_size * 8) in
       let sym_sndx = sym.st_shndx in
-      let code_bs =
-        bitstring_at_vaddr e sym_sndx sym_vaddr sym_size in
-      Some (parse_code_as_list code_bs)
+      begin match bitstring_at_vaddr e sym_sndx sym_vaddr sym_size with
+      | None -> None
+      | Some(code_bs) -> Some (parse_code_as_list code_bs)
+      end
   | _ -> None
+  end
 
 let code_of_sym_name (e: elf) (name: string): ecode option =
-  match ndx_of_sym_name e name with
+  begin match ndx_of_sym_name e name with
   | Some ndx -> code_of_sym_ndx e ndx
   | None     -> None
+  end