--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on October 2009 ---
nam nam wrote: > Good morning all > > I am using Frama-C Beryllium, and I want to use jessie plug-in to verify > some problems which I need to use float (or double) type number. I have > tried to use Simplify and Yices prover but they are not power enough to > prove the problems using float type number. > > Are there any ways to overcome this problem? Yes: Simplify is simply useless because does not know anything about real numbers, and Yices is not very powerful with them. You must install Alt-Ergo, Z3 and CVC3: see http://why.lri.fr/provers.en.html By the way: support for floating-point computation in Frama-C/Jessie is somewhat experimental. Please do not hesitate to share your attempts with us. See also: Hisseo projet web page: http://hisseo.saclay.inria.fr/ and its publications, in the "Documents" section - Claude > Thank you > D.T.Nam > > > ------------------------------------------------------------------------ > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss