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

[Frama-c-discuss] YASE, back to the roots



Hello again,

Thank You and granulations for the latest release.

But I have some problems to get started. Lets start with an example.
Following Function in separate files:


fill.h:

/*@
requires valid_range(first, last);
requires \valid_range(first, 0, last-first -1);
behavior is_not_empty:
assumes not_empty_range(first, last);
ensures \forall integer i;
0 <= i < last-first ==> first[i] == value;
*/
void fill (int* first, int* last, int value );

fill.c:

#include "fill.h"
void fill (int* first, int* last, int value )
{
int* it = first;
/*@
loop invariant first <= it <= last;
loop invariant \forall integer k; 0 <= k < it - first ==> first[k] == value;
*/
while (it != last)
*it++ = value;
}

I call Jessie:
frama-c -jessie-analysis -jessie-int-model exact -jessie-no-regions -jessie-gui fill.c

Now the problems:
-the loop invariant cannot be preserved, => am I missing an option or an annotation (it went fine on H and He)
-the declared int* it causes problems in pointer dereferencing
-Z3, CVC3, and Yices get stuck and wont abort, the timeout never worked on any release yet (on my pc)


I hope for help

Cheers
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081030/655b2aa5/attachment.html