--- layout: fc_discuss_archives title: Message 2 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,

Never mind. I realized that the global variable's state has changed before the termination of the fucntion. I replaced one of the ensures by \old then the first behavior got satisfied.

Best regards,
Dharma

-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Dharmalingam Ganesan
Sent: Monday, February 03, 2014 5:15 PM
To: Frama-C public discussion
Subject: [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
_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/2DRPoOd3gQcCQmjhOyMU-UqehNKVJeXObP33WapJeXObP33Xz9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSrtgohKWC_R-uhuouWZOWrbXT8I3DDQumKzp5dmXP_axVZicHs3jq9J4TvAm4TDNOb2pEVdTdw0PVkDjybE07-B2cJVSe08n8ixwCHIcfBisEeRNSeGWnIngBiPta6ToWHFuNt2lbdQEn8lrxrW0E-l9QUyW01_FgzbutyrososdCBInzGKBX5Q9kITixFtd402xoQg2PvQDaI3qpEVdEAQL