--- layout: fc_discuss_archives title: Message 122 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



Hi,

There is indeed a problem with the changes we made in the memory model of
the Jessie plugin. I think we'll have to patch the current release to
overcome this problem. If so, we will announce it on this list soon.

Yannick


On Thu, Oct 30, 2008 at 9:01 AM, Christoph Weber <
Christoph.Weber@first.fraunhofer.de> wrote:

>  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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>


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