--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on March 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



Hello Virgile,

Sorry for the more-than-very-late-reply. ;-) A few comments below.

Le 30/01/2019 à 19:40, Virgile Prevosto a écrit :
> 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.

I agree that such kind of abstraction might be needed in some cases but
is it really needed in that very simple case? Does it help to *easily*
prove wanted properties?


> 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;
> }
>
You might need to add some syntactic sugar but at least in the above
form I find your proposal overly complicated (e.g. use of
__internal_region).

Best regards,
david