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] VALID according to Unreachable Annotations

  • Subject: [Frama-c-discuss] VALID according to Unreachable Annotations
  • From: gpajela at GradCenter.cuny.edu (Gilbert Pajela)
  • Date: Thu, 10 May 2018 16:49:51 +0000
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>