cchecklink now reads segments instead of sections

cchecklink is now using program header information to figure out the
initial address space of the program, rather than the information in the
parent section of each symbol. This decouples the resolution of symbols
from inaccurate section information, reflecting more the actual program
loading. Additionally, a -relaxed option has been added to deal with
some strange ELFs, for instance when symbols data is dynamically
bootstrapped from another place by boot code different than the program
loader.

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

1 files changed, 7 insertions, 2 deletions

diff --git a/checklink/Validator.ml b/checklink/Validator.ml
index c413c75..55e4da1 100644
--- a/checklink/Validator.ml
+++ b/checklink/Validator.ml
@@ -10,9 +10,10 @@ let option_bytefuzz = ref false
 let option_printelf = ref false
 
 let set_elf_file s =
-  match !elf_file with
+  begin match !elf_file with
   | None -> elf_file := Some s
   | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line")
+  end
 
 let options = [
   "-exe <filename>", Arg.String set_elf_file,
@@ -33,6 +34,9 @@ let options = [
   "Random fuzz testing byte per byte";
   "-debugfuzz", Arg.Set Fuzz.fuzz_debug,
   "Print a detailed trace of ongoing fuzz testing";
+  "-relaxed", Arg.Set ELF_parsers.relaxed,
+  "Allows the following behaviors in the ELF parser:
+\t* Use of a fallback heuristic to resolve symbols bootstrapped at load time";
 ]
 
 let anonymous arg =
@@ -49,7 +53,7 @@ Options are:"
 
 let _ =
   Arg.parse options anonymous usage;
-  match !elf_file with
+  begin match !elf_file with
   | None ->
       Arg.usage options usage;
       exit 2
@@ -67,3 +71,4 @@ let _ =
       end else begin
         check_elf_dump elffilename sdumps
       end
+  end