--- layout: fc_discuss_archives title: Message 92 from Frama-C-discuss on November 2009 ---
??????? ?????? wrote: > Wow, thanks! It really seems to work. But I'm not sure I got the idea > in its entirety. Do you mean that Jessie restricts "a" and "b" to be > in the same block just when it comes across any order relation between > these pointers? So, for example, if I want these pointers to be in the > same block, but don't want to specify any restriction (so that > pointers can overlap and all that), I'll just need to write something > like "requires (a == b) || (a < b) || (a > b)", right? > Indeed yes. Or simpler : (a == b) && (a != b) Sure it is not nice, but it is only a work-around. Generally speaking, I am interested in any similar example of that need, a part from the swap function which seems to be the only example so far... - Claude > - Dmitry > > 2009/11/24 Claude Marche <Claude.Marche at inria.fr > <mailto:Claude.Marche at inria.fr>> > > > The reason is that swap is first interpreted as if a and b were in > different block, whereas you call it on pointers to the same block. > A work around is to add a precondition that restrict a and b to be in > the same block, and anyway you need something to specify that they do > not overlap, e.g > > requires (a==b) || (a + size <= b) || (b + size <= a); > > > - Claude > > ------------------------------------------------------------------------ > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |