--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2019 ---
Hello David, As Rafael suggested, wouldn't be possible to have some ACSL specific > syntax to refer such static variable into contracts? Use of static is > one of the rare case of modularity feature in C and it is widely used in > industrial C code. This is a long term issue that at least needs a > work-around if a clean fix cannot be found. > > Building on your example, one could imagine that variable counter of a.c > could *only* be accessed in contracts through "a_counter" name. > Therefore in a.h one would be forced to use "a_counter" name and that > contract would be valid in both a.c and in b.c. > > Indeed, being forced by the formal spec to expose more of the implementation can't be seen as moving in the good direction ð. I tend to think that what is missing there in ACSL is the possibility to have two contracts for the same function, a "private" one (with full access to static (global) variable), and a "public" one, which would be more abstract. Of course, we would also need some way to express the bindings between both contracts. Going back to the counter example, something like that might fit the bill in terms of "public" contract /*@ ghost int* __internal_region; */ /*@ axiomatic Internal { logic integer counter{L} reads *__internal_region; axiom valid_region: \valid(__internal_region); } */ /*@ requires counter < 1000; //cheap way to get rid of overflows assigns *__internal_region; ensures counter == \at(counter, Pre) + 1; ensures \result == counter; */ int f(void); In order to show that the following definition respects the contract, we'd then need to have ACSL extensions for defining the link between the counter logic variable and c static variable (i.e. generating the 'binding' assert, and setting their status to Valid, possibly after generating additional lemmas/verification conditions if the relationship between the internal state of the function and its logic model is not as simple as is the case here) int f() { static int c = 0; //@ assert binding: __internal_region == &c; //@ assert binding: c == counter; c++; //@ assert binding: c == counter; return c; } Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190130/57bbf682/attachment.html>