--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on November 2008 ---
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