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] Contract status dependences

  • Subject: [Frama-c-discuss] Contract status dependences
  • From: gpajela at GradCenter.cuny.edu (Gilbert Pajela)
  • Date: Sat, 23 Apr 2016 05:29:19 +0000
Hello,


According to Section 7.2 of the Frama-C User Manual, when proving the Hoare triple {A}S{B}, the WP plugin sets B to true dependent on A. However, this seems inconsistent with what happens when I prove a statement contract with requires clause A and ensures clause B, since the ball next to B turns full green. Why does this happen? Also, when looking at the dependencies graph for property B, it doesn't show the dependency from B to A. Why not?


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