--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP question



Hi,

I used WP for the following two equivalent behaviours. I started with the first behaviour, WP claimed unknown.

behavior STOP_DRUG_MR_Pos:
      assumes msgId == MSG_CMD_STOP_DRUG;
      assumes gfMaintenance_Rate > 0;
      ensures gfPreviousMR == gfMaintenance_Rate;
      ensures gfMaintenance_Rate == 0;
      ensures gbDrugTerm == true;


I rewrote the above by the following. WP claimed valid. 

   behavior STOP_DRUG_MR_Pos_2:
      ensures msgId == MSG_CMD_STOP_DRUG && gfMaintenance_Rate > 0 ==> gfPreviousMR == gfMaintenance_Rate && gfMaintenance_Rate == 0 && gbDrugTerm == true;


I'm confused why the first one is considered unknown whereas the second one is valid, although both the behaviours are the same.

Any comments?
Dharma