--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Function-local static variables and preprocessor variables




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
}