From 521dac4e0d950e6128b266b27eac1875d79200f1 Mon Sep 17 00:00:00 2001 From: varobert Date: Thu, 10 May 2012 07:53:57 +0000 Subject: 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 --- checklink/Frameworks.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'checklink/Frameworks.ml') 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 - - -- cgit v1.2.3