From 9ea00d39bb32c1f188f1af2745c3368da6a349c1 Mon Sep 17 00:00:00 2001 From: varobert Date: Thu, 24 May 2012 15:00:56 +0000 Subject: 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 --- checklink/Library.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'checklink/Library.ml') 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. *) -- cgit v1.2.3