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

[Frama-c-discuss] Jessie question



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