diff options
| author |  varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-10 07:53:57 +0000 |
|---|---|---|
| committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-10 07:53:57 +0000 |
| commit | 521dac4e0d950e6128b266b27eac1875d79200f1 (patch) | |
| tree | f8b73847a64c769264065c88a31a413f3c3511e4 /checklink/Frameworks.ml | |
| parent | a6044b4a4d38354411cbf535472776f4d5bb30d5 (diff) | |
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
Diffstat (limited to 'checklink/Frameworks.ml')
| -rw-r--r-- | checklink/Frameworks.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index 4e98735..46778e2 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -136,7 +136,7 @@ let stub_ident_to_vaddr = { let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc) (efw: e_framework): e_framework = assert (0l <= start && 0l < length); - let stop = Int32.(sub (add start length) 1l) in + let stop = Safe32.(start + length - 1l) in { efw with chkd_bytes_list = @@ -196,5 +196,3 @@ let string_of_byte_chunk_desc = function | Float_literal(f) -> "Float literal: " ^ string_of_float f | Padding -> "Padding" | Unknown(s) -> " ??? " ^ s - - |