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 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>