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

> 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

> 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++;
}

> I would say that the first mistake could be that you tried those using
the WP plug-in, whereas these examples were proved using Jessie instead.

My bad, indeed! Thank you for the book suggestion.

Thank you very much for your information and help!

Am Mo., 21. Jan. 2019 um 20:11 Uhr schrieb Claude Marché <
Claude.Marche at inria.fr>:

>
>
> Le 21/01/2019 à 17:20, Rafael Bachmann a écrit :
> > Apart from these (I may be wrong, usually am), I had difficulties finding
> > good documentation regarding floating point numbers.
> > This habilitation:https://hal.inria.fr/tel-01089643/document  contains
> many
> > very good examples, none of which I can reproduce (the author uses Coq
> > sometimes, but in other cases gappa suffices). On my machine, the
> > verification simply fails. Might something be wrong with my Frama-C
> > installation?
>
> I would say that the first mistake could be that you tried those using
> the WP plug-in, whereas these examples were proved using Jessie instead.
>
> I believe that they should be reproducible even with recent versions of
> Frama-C.
>
> For the proper source codes and proof sessions you may look at
> http://toccata.lri.fr/gallery/fp.en.html and
> https://www.lri.fr/~sboldo/research.html
>
> For more documentation: see also
>
> @book{BM17,
>    title = {Computer Arithmetic and Formal Proofs: Verifying
> Floating-point Algorithms with the {Coq} System},
>    author = {Boldo, Sylvie and Melquiond, Guillaume},
>    hal = {https://hal.inria.fr/hal-01632617},
>    publisher = {ISTE Press - Elsevier},
>    year = 2017,
>    month = dec
> }
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190122/08fee868/attachment.html>