Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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