--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on June 2014 ---
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