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: Claude.Marche at inria.fr (Claude Marché)
  • Date: Mon, 21 Jan 2019 20:10:24 +0100
  • In-reply-to: <CAHnaJbvwMbZWLiJ=gdm4Bmi-xELx4MY6qUMGigXRyv29KdAYJg@mail.gmail.com>
  • References: <CAHnaJbvwMbZWLiJ=gdm4Bmi-xELx4MY6qUMGigXRyv29KdAYJg@mail.gmail.com>

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
}