Frama-C A long time ago, John Regehr wrote a blog post about a 3-3 split vote that occurred while he was finding bugs in C compilers through differential testing. John could have included Frama-C's value analysis in his set of C implementations and then the vote would have been 4-3 for...
Read MoreThe documentation of the correctly-rounded CRlibm floating-point library states for the difficult pow() function (p. 159): Directed rounding requires additional work in particular in subnormal handling and in exact case management. There are more exact cases in directed rounding modes therefore the performance should also be inferior. The phrase “exact...
Read More… but that's only because I created it. If you are more familiar than me with Wikipedia etiquette feel free to adjust edit or delete this page. Also although a Wikipedia account is necessary to create a page I think it is not required for editing so you can add...
Read MoreIntroduction It started innocently enough. My colleagues were talking of supporting target compilers with excess floating-point precision. We saw that if analyzing programs destined to be compiled with strict IEEE 754 compilers was a lovely Spring day at the beach analyzing for compilers that allow excess precision was Normandy in...
Read MoreThere has been talk recently amongst my colleagues of Frama-C-wide support for compilation platforms that define FLT_EVAL_METHOD as 2. Remember that this compiler-set value, introduced in C99, means that all floating-point computations in the C program are made with long double precision, even if the type of the expressions they...
Read More