Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] How to use a predicate with OCaml code but not by hand?
- Subject: [Frama-c-discuss] How to use a predicate with OCaml code but not by hand?
- From: njucslzh0714 at gmail.com (刘自恒)
- Date: Fri, 7 Oct 2011 23:09:32 +0800
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>
- Follow-Ups:
- [Frama-c-discuss] How to use a predicate with OCaml code but not by hand?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] How to use a predicate with OCaml code but not by hand?
- Prev by Date: [Frama-c-discuss] using ptests
- Next by Date: [Frama-c-discuss] How to use a predicate with OCaml code but not by hand?
- Previous by thread: [Frama-c-discuss] using ptests
- Next by thread: [Frama-c-discuss] How to use a predicate with OCaml code but not by hand?
- Index(es):