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] problem with an example in acsl 1.4 doc

  • Subject: [Frama-c-discuss] problem with an example in acsl 1.4 doc
  • From: chengeng4001 at gmail.com (geng chen)
  • Date: Thu, 22 Oct 2009 14:13:07 +0800
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