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] Fwd: Frama-C max_sqe question

  • Subject: [Frama-c-discuss] Fwd: Frama-C max_sqe question
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Tue, 10 Jun 2014 18:05:17 +0200
  • In-reply-to: <5397291A.2010608@inria.fr>
  • References: <1402305133.31114.YahooMailNeo@web140902.mail.bf1.yahoo.com> <5397291A.2010608@inria.fr>
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