--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2014 ---
Small correction: please replace "f" by "open". -----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: Sunday, February 09, 2014 12:19 AM To: Frama-C public discussion Subject: [Frama-c-discuss] State-based contracts in ACSL? Hi, I have a function Bool open(int id); Informally, f should return true for every new id otherwise returns false. For example, open(1) = true; open(1) = false; I read the documentation of ACSL but could not locate anything similar to the above scenario. It seems ghost variables may contribute here(?), but assume we are not allowed to modify the existing definition of f nor we do not have access to any interface to check whether id is already in use . Any comments? Dharma _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://cp.mcafee.com/d/avndy0A83hJ5AQsECzBdB4syrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCQvtKetjvW_8Kcfcf6zDHTbFFzxT9I9LCzBxfBHEShhlLtzBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdIcec6PiSbNRniZyW4GmrFgQKCy0oDI_bAdFW1EwJm4UXqt3h1a1Ew418o2F8SMYr75XFvb1Qw1U