--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2014 ---
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