--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on October 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with an example in acsl 1.4 doc



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