--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on February 2014 ---
Hello, Le 09/02/2014 06:19, Dharmalingam Ganesan a ?crit : > Bool open(int id); > > Informally, f should return true for every new id otherwise returns false. open(), not f(). How open() is implemented? I assume it looks at some global variables recording the current state. I would refer to this global state in open()'s contract. Best regards, david