--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Fwd: Frama-C max_sqe question



Hello,

2014-06-10 17:49 GMT+02:00 Claude March? <Claude.Marche at inria.fr>:

> * ACSL proposes, afaik, a built-in predicate \num_of for such a purpose
>
> * Anyway, I bet it is not implemented in Frama-C kernel. A fortiori,
> plug-ins Jessie and WP do not support it.
>

Well, I'm afraid you lost your bet:

virgile at is220177:~$ cat numof.c
/*@
  requires \valid(a+(0 .. length - 1));
  assigns \nothing;
  ensures \result == \numof(0,length-1,\lambda integer i; a[i] == 0); */
int count_zero(int* a, int length) {
  int res = 0;
  /*@
    loop invariant 0<=i<=length;
    loop assigns i, res;
    loop invariant res == \numof(0,i-1,\lambda integer j; a[j] == 0);
  */
  for(int i = 0; i < length; i++)
    if (a[i] == 0) res++;
  return res;
}

virgile at is220177:~$ frama-c -version
Version: Neon-20140301
[...]

virgile at is220177:~$ frama-c -print numof.c
[kernel] preprocessing with "gcc -C -E -I.  numof.c"
/* Generated by Frama-C */
/*@ requires \valid(a+(0 .. length-1));
    ensures
      \result ? \numof(0, \old(length)-1, \lambda ? i; *(\old(a)+i)?0);
    assigns \nothing;
 */
int count_zero(int *a, int length)
{
  int res;
  res = 0;
  {
    int i;
    i = 0;
    /*@ loop invariant 0 ? i ? i ? length;
        loop invariant res ? \numof(0, i-1, \lambda ? j; *(a+j)?0);
        loop assigns i, res;
    */
    while (i < length) {
      if (*(a + i) == 0) res ++;
      i ++;
    }
  }
  return res;
}

That said, WP supports neither \numof nor \lambda, and I don't think
that Jessie performs better in that domain (maybe Jessie3 when it'll
be out?), so you're right, defining your own predicate is probably the
best way to proceed.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile