--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] VALID according to Unreachable Annotations



Hello,

I just now noticed a difference in the consolidated property status reported by Frama-C since the Phosphorus version that I don't understand. Let's say I use the following as an input program to Frama-C:

int x;
/*@ ensures x == 3; */
{
  x = 3;
  /*@ loop invariant x >= 0; */
  while (x > 0) {
    x --;
  }
}

Note that the ensures clause is false. Back in the Silicon version of Frama-C, if I try to use WP to prove the ensures clause, the consolidated status reported by Frama-C would say, "unknown (tried by Wp.typed)", and the circle next to the ensures clause in the GUI would turn yellow. However, from Phosphorus (the version after Silicon) to the current version, with the same program, Frama-C instead reports, "VALID according to Unreachable Annotations", and the circle turns green instead of yellow.

What does "Unreachable Annotations" exactly mean and under what conditions would it be triggered? I wouldn't think that the ensures clause in the example above is unreachable since the while loop does terminate.

Thanks,
Gilbert
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180510/bdf36306/attachment.html>