Added small data area support to checklink

Accesses to small data areas are dynamically resolved by constructing a
mapping from registers to virtual addresses they are supposed to point
to. This mapping is reported.

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

1 files changed, 11 insertions, 1 deletions

diff --git a/checklink/Library.ml b/checklink/Library.ml
index bb0d217..0259039 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -3,6 +3,7 @@ open BinPos
 
 type bitstring = Bitstring.bitstring
 
+module IntMap = Map.Make(struct type t = int let compare = compare end)
 module StringMap = Map.Make (String)
 
 let is_some: 'a option -> bool = function
@@ -24,13 +25,22 @@ let is_ok: 'a or_err -> bool = function
 | OK(_) -> true
 | ERR(_) -> false
 
+let is_err x = not (is_ok x)
+
 let from_ok: 'a or_err -> 'a = function
 | OK(x) -> x
-| ERR(_) -> raise Not_found
+| ERR(_) -> assert false
+
+let from_err: 'a or_err -> string = function
+| OK(_) -> assert false
+| ERR(s) -> s
 
 let filter_ok (l: 'a or_err list): 'a list =
   List.(map from_ok (filter is_ok l))
 
+let filter_err (l: 'a or_err list): string list =
+  List.(map from_err (filter is_err l))
+
 external id : 'a -> 'a = "%identity"
 
 (** Checks for existence of an array element satisfying a condition, and returns