--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2011 ---
Hi, First, an example as below: /*@ predicate is_valid_int_range(int* p, int n) = (0 <= n) && \valid_range(p,0,n-1); lemma foo: \forall int* p,n; is_valid_int_range(p,n) <==> \valid_range(p,0,n-1); */ /*@ requires is_valid_int_range(a, n); requires is_valid_int_range(b, n); assigns \nothing; behavior all_equal: assumes \forall int i; 0 <= i < n ==> a[i] == b[i]; ensures \result == 1; behavior some_not_equal: assumes \exists int i; 0 <= i < n && a[i] != b[i]; ensures \result == 0; complete behaviors all_equal, some_not_equal; disjoint behaviors all_equal, some_not_equal; */ int equal(const int* a, int n, const int* b) { for (int i = 0; i < n; i++) if (a[i] == b[i]) { count = count + 1; } return count; } Now how can I use the predicate "is_valid_int_range" with OCaml code but not by hand if it is pre-defined somewhere? That is the annotations such as "requires is_valid_int_range(a, n);" can be generated automatically. Its name and its profile have been extracted. Best Wishes. Henry -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111007/40bbc45f/attachment.htm>