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