I am using Frama-C to verify the following program and trying to obtain program states during the verification. For example, I try to print P0 in the following code.

requires x <= y;
ensures x = y;
void test(int x, int y) {
  /*@ loop invariant x <= y;
 */
  while(x <= y) {
    x = x + 1; // P1
  }
}

Could you please show me how to obtain the program state P1?

Many thanks,
Loc