--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on April 2010 ---
Hi, consider the program /*@ 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? Thanks, best regards Jorge Sousa Pinto