cchecklink continues when sections overlap

cchecklink now reports overlapping sections but keeps analyzing. Error
messages have also been made clearer.

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

1 files changed, 12 insertions, 0 deletions

diff --git a/checklink/Library.ml b/checklink/Library.ml
index f55d9de..0ce3bcd 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -43,6 +43,18 @@ let filter_err (l: 'a or_err list): string list =
 
 external id : 'a -> 'a = "%identity"
 
+(** [a; a + 1; ... ; b - 1; b] *)
+let list_ab (a: int) (b: int): int list =
+  let rec list_ab_aux a b res =
+    if b < a
+    then res
+    else list_ab_aux a (b - 1) (b :: res)
+  in list_ab_aux a b []
+
+(** [0; 1; ...; n - 1] *)
+let list_n (n: int): int list =
+  list_ab 0 (n - 1)
+
 (** Checks for existence of an array element satisfying a condition, and returns
     its index if it exists.
 *)