Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Function-local static variables and preprocessor variables

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