--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on April 2010 ---
Pascal Cuoq wrote: >> Now the postcondition cannot be discharged, as expected. But doesn't this >> mean that the first program should not be considered correct? As explain in the old thread mentioned by Pascal, the first program is proved assuming that c and &y are in different memory blocks. If your attempt to call it in a context where it is not the case, it will fail to prove. > I hear that some of the information in this old thread is now obsolete: Pascal, I don't understand why you think the information is obsolete. It seems to be a similar case to me, with the same answer. - Claude > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000958.html > > The basic fact remains that it is technically impossible to say anything at all > about a C function that manipulates pointers without any hypotheses. > Jessie will make these hypotheses on its own (but it will force you to prove > that they apply at the call site). > > Although you have written the same preconditions, Jessie is not using the > same hypotheses in your two examples. I think that in the first one it is > assuming that you mean c and &y to be separated since you didn't > specify anything. But I may have misunderstood how the new behavior > works. > > Pascal > > _______________________________________________ > 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 | http://maps.google.fr/maps?q=48.70963,2.17513+%28Claude+March%C3%A9%27s+Office%29