Merge branch 'master' into pure-makefiles

2 files changed, 20 insertions, 26 deletions

diff --git a/checklink/Bitstring_utils.ml b/checklink/Bitstring_utils.ml
index 2253b63f..3218f898 100644
--- a/checklink/Bitstring_utils.ml
+++ b/checklink/Bitstring_utils.ml
@@ -9,6 +9,13 @@ type bitstring = Bitstring.bitstring
     bitstring may be longer.
     @param size number of bits to check
 *)
+
+let is_zeros (bs: bitstring) (size: int): bool =
+  Bitstring.bitstring_length bs >= size
+  && Bitstring.is_zeroes_bitstring (Bitstring.subbitstring bs 0 size)
+
+(*
+
 let rec is_zeros (bs: bitstring) (size: int): bool =
   size = 0 ||
   if size >= 64
@@ -23,3 +30,4 @@ let rec is_zeros (bs: bitstring) (size: int): bool =
     | { 0L : size : int } -> true
     | { _ } -> false
   )
+*)
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 5213b266..db0159c4 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -69,8 +69,8 @@ let name_of_section_Linux: section_name -> string = function
 | Section_text -> ".text"
 | Section_data i -> if i then ".data" else "COMM"
 | Section_small_data i -> if i then ".sdata" else ".sbss"
-| Section_const -> ".rodata"
-| Section_small_const -> ".sdata2"
+| Section_const i -> if i then ".rodata" else "COMM"
+| Section_small_const i -> if i then ".sdata2" else "COMM"
 | Section_string -> ".rodata"
 | Section_literal -> ".rodata.cst8"
 | Section_jumptable -> ".text"
@@ -79,10 +79,10 @@ let name_of_section_Linux: section_name -> string = function
 (** Adapted from CompCert *)
 let name_of_section_Diab: section_name -> string = function
 | Section_text -> ".text"
-| Section_data i -> if i then ".data" else ".bss"
+| Section_data i -> if i then ".data" else "COMM"
 | Section_small_data i -> if i then ".sdata" else ".sbss"
-| Section_const -> ".text"
-| Section_small_const -> ".sdata2"
+| Section_const _ -> ".text"
+| Section_small_const _ -> ".sdata2"
 | Section_string -> ".text"
 | Section_literal -> ".text"
 | Section_jumptable -> ".text"
@@ -91,7 +91,6 @@ let name_of_section_Diab: section_name -> string = function
 (** Taken from CompCert *)
 let name_of_section: section_name -> string =
   begin match Configuration.system with
-  | "macosx" -> fatal "Unsupported CompCert configuration: macosx"
   | "linux"  -> name_of_section_Linux
   | "diab"   -> name_of_section_Diab
   | _        -> fatal "Unsupported CompCert configuration"
@@ -535,12 +534,6 @@ let check_label_existence ffw =
     had the expected [size].
 *)
 let rec match_jmptbl lbllist vaddr size ffw =
-  let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in
-  let jmptbl_section =
-    match atom.a_sections with
-    | [_; _; j] -> j
-    | _ -> Section_jumptable
-  in
   let rec match_jmptbl_aux lbllist bs ffw =
     match lbllist with
     | [] -> OK ffw
@@ -556,21 +549,14 @@ let rec match_jmptbl lbllist vaddr size ffw =
     )
   in
   let elf = ffw.sf.ef.elf in
-  begin match section_at_vaddr elf vaddr with
+  begin match bitstring_at_vaddr elf vaddr size with
   | None -> ERR("No section for the jumptable")
-  | Some(sndx) ->
-      begin match bitstring_at_vaddr elf vaddr size with
-      | None -> ERR("")
-      | Some(bs, pofs, psize) ->
-          ffw
-          >>> (ff_sf ^%=
-              match_sections_name jmptbl_section elf.e_shdra.(sndx).sh_name
-          )
-          >>> match_jmptbl_aux lbllist bs
-          >>^ (ff_ef ^%=
-              add_range pofs psize 0 Jumptable
-          )
-      end
+  | Some(bs, pofs, psize) ->
+      ffw
+        >>> match_jmptbl_aux lbllist bs
+        >>^ (ff_ef ^%=
+               add_range pofs psize 0 Jumptable
+            )
   end
 
 let match_bo_bt_bool bo =