--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on October 2009 ---
hi, everyone I've met a problem with the example in acsl 1.4 document. I copy the code from page 36 here is the code: ------------------------------------------------------------------------------------------------------ /*@ requires n >= 0 && \valid(t+(0..n-1)); @ assigns \nothing; @ ensures -1 <= \result <= n-1; @ behavior success; @ ensures \result >= 0 ==> t[\result] == v; @ behavior failure: @ assumes t_is_sorted : \forall integer k1, int k2; @ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2]; @ ensures \result == -1 ==> @ \forall integer k; 0 <= k < n ==> t[k] != v; @*/ int bsearch(double t[], int n, double v) { int l = 0, u = n - 1; /*@ loop invariant 0 <= l && u <= n-1; @ for failure: loop invariant @ \forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u; @*/ while (l <= u) { int m = l + (u -1) / 2; //better than (l+u)/2 if (t[m] < v) l = m + 1; else if (t[m] > v) u = m - 1; else return m; } return -1; } ----------------------------------------------------------------------------------------------------- and I use the command frama-c -jessie bsearch.c, the following message came out: ----------------------------------------------------------------------------------------------------- tang at tang-desktop:~/Desktop/bsearch$ frama-c -jessie ./bsearch.c [kernel] preprocessing with "gcc -C -E -I. -dD ./bsearch.c" ./bsearch.c:7:[kernel] user error: syntax error while parsing annotation [kernel] user error: skipping file "./bsearch.c" that has errors. [kernel] Plugin kernel aborted because of invalid user input(s). ----------------------------------------------------------------------------------------------------- I've installed Why 2.21and Frama-C Beryllium 2(all of them are the latest version). Is there anything wrong in the code or my system? Best regards, Chen -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091022/d974fa51/attachment.htm