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,

Le mar. 22 janv. 2019 à 12:55, Rafael Bachmann <mediumendian at gmail.com> a
écrit :

> > In particular, this change will not help when you're writing a function
> contract in a .h for a function whose implementation
> is using a static variable that only exists in the .c.
>
> CIL handles that by moving local statics to global scope and prefixing the
> function name, regardless of where the prototype is located (even header
> file - just tried). That may be
>
>
Sorry, I should have made myself clearer: the issue will arise if you have
more than one .c file, i.e. something like

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.


> > you might be able to have some results by using a (global) ghost
> variable to store the address of your static variable, and use it in the
> contracts, but I fear that it can quickly become awkard.
>
> Do you mean something like this?
> //@ ghost uint64_t *ghost_adress = NULL;
> /*@ require *(ghost_adress) < 10;
> */
> uint64_t count() {
>     static uint64_t counter = 0;
>     //@ ghost ghost_adress = &counter;
>     return counter++;
> }
>
>
Exactly, except that you can't really use *ghost_adress in the requires,
since for the first call to count it will be NULL. Furthermore, you'll need
to specifiy everything the function does in terms of *ghost_adress, and I'm
not really sure how you would express the fact that when entering the
function ghost_adress points to counter (otherwise the requires will not be
very useful). But unfortunately, I think that's the best you can get with
the current state of ACSL.

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/20190122/3bdf9992/attachment.html>