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] YASE, back to the roots

Hi,

Notice that stating equality of pointers in annotations implies they belong
to the same block (which is not the case for inequalities), maybe this can
save you some annotations. Unfortunately, this change is necessary for
correction.

We are going to issue a new version of the Lithium release in the next days,
with all necessary binaries.

Yannick


On Wed, Nov 5, 2008 at 7:55 PM, Jens Gerlach <
jens.gerlach@first.fraunhofer.de> wrote:

> 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
>
>


-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081106/2e215aa1/attachment.htm