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

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



Hello Yannick,

thanks for your explanation. As I see it we have to change
a lot in the specifications written until now.

So far we are using Frama-C on Windows and Mac OS X.
For Windows we would prefer a binary version.
For Mac OS X we are used to compile Frama-C, so a patch would probably  
be fine.

Jens

Am 05.11.2008 um 16:49 schrieb Yannick Moy:

> Hi,
>
> Coming back to the problem Christoph signaled last week ...
>
> We corrected the Jessie plugin to remove the regression you  
> observed, but this requires stating when pointers belong to the same  
> block. Indeed, equality of pointer values in C is not the same as  
> equality of the logic pointer entities in our memory model. Thus, in  
> the example you showed us, stating that [first <= last] in the  
> precondition does not guarantee that first and last belong to the  
> same block, which is later on needed to prove the loop invariant.  
> Thus,
> you must state in the precondition and the loop invariant that some  
> pointers belong to the same allocated block of memory. There is no  
> predefined construct in ACSL to state this, so we translate equality  
> of base addresses in Jessie to express precisely that, although it  
> would be better expressed with a special construct in the future.
>
> Thus, your example with new annotations looks like:
>
> /*@
>   @requires \valid_range(first, 0, last-first -1)
>   @      && first <= last && \base_addr(first) == \base_addr(last);
>   @behavior is_not_empty:
>   @  ensures \forall integer i;
>   @  0 <= i < last-first ==> first[i] == value;
> */
> void fill (int* first, int* last, int value )
> {
>   int* it = first;
>
>   /*@
>     @loop invariant first <= it <= last
>     @            && \base_addr(first) == \base_addr(it)
>     @            && \base_addr(last) == \base_addr(it);
>     @loop invariant \forall integer k; 0 <= k < it - first ==>  
> first[k] == value;
>   */
>   while (it != last)
>     *it++ = value;
> }
>
> With our corrections, all VC are now proved by Alt-Ergo, Simplify  
> and Z3.
>
> Let us know how you would like a patch, before we build a new  
> release. Can we send you binaries for linux?
>
> Cheers,
>
> Yannick
>
>
> On Fri, Oct 31, 2008 at 10:08 AM, Yannick Moy  
> <yannick.moy@gmail.com> wrote:
> Hi again,
>
> I am sorry to delay the definite answer to your problem to next  
> Wednesday, when other members of the team come back from holidays.  
> The problem you faced is directly linked to some corrections we made  
> on our memory model, and there are issues I cannot decide to solve  
> one way or another by myself.
>
> Sorry for the inconvenience, we will send you a patch asap next week.
>
> Yannick
>
>
>
> On Thu, Oct 30, 2008 at 9:51 AM, Pascal Cuoq <Pascal.Cuoq@cea.fr>  
> wrote:
>  I think we'll have to patch the current release to overcome this  
> problem. If so, we will announce it on this list soon.
>
> Indeed, the release was a little bit rushed, but it's okay
> because the version is clearly labeled as "beta" :)
>
> I would like to take this opportunity to encourage plug-in
> developers to work with the users of their plug-ins
> to make the next iteration of Frama-C (to be released in
> the next few days) as stable as possible.
>
> Frama-C is Open Source and Frama-C's users
> are bright and motivated people.
> It is probably a good, efficient way
> to work to send them patches in order to
> fix the problem that is blocking them and allow them
> to further their tests, so that the next release may work
> really well for what is supposed to work already.
>
> Thanks to everyone on this list for their contributions.
>
> Pascal
>
>
>
>
> -- 
> Yannick
>
>
>
> -- 
> Yannick
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss


-- 

Dr.-Ing. Jens Gerlach
Eingebettete Systeme - EST
Tel.: +49 (0)30 6392 1841
Fax.: +49 (0)30 6392 1805
E-Mail: jens.gerlach@first.fraunhofer.de

Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST
Kekul?stra?e 7
12489 Berlin
Germany
http://www.first.fraunhofer.de


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081105/4cdbf892/attachment.html