diff options
author | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-24 15:00:56 +0000 |
---|---|---|
committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-24 15:00:56 +0000 |
commit | 9ea00d39bb32c1f188f1af2745c3368da6a349c1 (patch) | |
tree | a433d427fb7e0e2dee5598973a1f21328f19e973 /checklink/Library.ml | |
parent | b119b949b2a370d9a61b2844b982669f7aa47d01 (diff) | |
download | compcert-9ea00d39bb32c1f188f1af2745c3368da6a349c1.tar.gz compcert-9ea00d39bb32c1f188f1af2745c3368da6a349c1.zip |
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
Diffstat (limited to 'checklink/Library.ml')
-rw-r--r-- | checklink/Library.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/checklink/Library.ml b/checklink/Library.ml index f55d9dea..0ce3bcd9 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. *) |