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

[Frama-c-discuss] Using Frama-C as Caduceus



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