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: mediumendian at gmail.com (Rafael Bachmann)
- Date: Tue, 22 Jan 2019 12:55:07 +0100
- In-reply-to: <756f93bc-4c9e-c4ba-af34-126d6e50076a@inria.fr>
- References: <CAHnaJbvwMbZWLiJ=gdm4Bmi-xELx4MY6qUMGigXRyv29KdAYJg@mail.gmail.com> <756f93bc-4c9e-c4ba-af34-126d6e50076a@inria.fr>
> 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>
- Follow-Ups:
- [Frama-c-discuss] Function-local static variables and preprocessor variables
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Function-local static variables and preprocessor variables
- References:
- [Frama-c-discuss] Function-local static variables and preprocessor variables
- From: rafael.bachmann.93 at gmail.com (Rafael Bachmann)
- [Frama-c-discuss] Function-local static variables and preprocessor variables
- From: Claude.Marche at inria.fr (Claude Marché)
- [Frama-c-discuss] Function-local static variables and preprocessor variables
- Prev by Date: [Frama-c-discuss] Function-local static variables and preprocessor variables
- Next by Date: [Frama-c-discuss] Function-local static variables and preprocessor variables
- Previous by thread: [Frama-c-discuss] Function-local static variables and preprocessor variables
- Next by thread: [Frama-c-discuss] Function-local static variables and preprocessor variables
- Index(es):