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

  • Subject: [Frama-c-discuss] Function-local static variables and preprocessor variables
  • From: David.MENTRE at bentobako.org (David MENTRÉ)
  • Date: Sun, 17 Mar 2019 11:39:42 +0100
  • In-reply-to: <CA+yPOVjYQ1Nari9Vm3kA63ZwUWW7eXg4cebYWLSM2nUd4SL=vA@mail.gmail.com>
  • References: <CAHnaJbvwMbZWLiJ=gdm4Bmi-xELx4MY6qUMGigXRyv29KdAYJg@mail.gmail.com> <756f93bc-4c9e-c4ba-af34-126d6e50076a@inria.fr> <CAP+XvKYQ5p4RjL0fDx7PJB8LMvAPZR5h3TMYW_wOELjQT6ynHQ@mail.gmail.com> <CA+yPOVghauPWrKoTWvKPxwun=ynVErsurrFZZFuH01aHKWxbqw@mail.gmail.com> <2181809a-10dc-c0bd-9d9c-9adb1806c239@bentobako.org> <CA+yPOVjYQ1Nari9Vm3kA63ZwUWW7eXg4cebYWLSM2nUd4SL=vA@mail.gmail.com>
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