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

Hello,

On Wed, Apr 28, 2010 at 1:01 AM, Jorge Sousa Pinto <jsp at di.uminho.pt> wrote:
> /*@ requires \valid(c);
> ?@ ensures *c == 10 && y == 20;
> ?@*/
> void q(int *c)
> {
> ?y = 20;
> ?*c = 10;
> }
>
> The program is proved correct with my installation of Frama-C, but now
> suppose the precondition is strengthened as follows
>
> /*@ requires \valid(c) && c==&y;
> ?@ ensures *c == 10 && y == 20;
> ?@*/
> void q(int *c)
> {
> ?y = 20;
> ?*c = 10;
> }
>
> Now the postcondition cannot be discharged, as expected. But doesn't this
> mean that the first program should not be considered correct?

I hear that some of the information in this old thread is now obsolete:

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