--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on January 2019 ---
Hello Virgile, Le 22/01/2019 à 14:36, Virgile Prevosto a écrit : > a.h: > > /*@ requires counter < 10 */ > extern int f(void); > > a.c: > static unsigned int counter; > > #include "a.h" > > int f(void) { return counter++; } > > b.c: > #include "a.h" > > int main () { >  return f(); > } > > In this context, the contract of f as seen from the point of view of > b.c is ill-formed, and the only way to make it type-check is to put an > extern declaration of counter in a.h, and to remove the static from > the tentative defiinition of counter in a.c (otherwise, the counter > from b.c will not be the same as the one from a.c). If you only have a > single translation unit, then indeed there's no problem. 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. Best regards, david