--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie question




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