Blog

Bug in Nitrogen's value analysis
Pascal Cuoq on 23 November 2011

In the course of restructuring the value analysis, I noticed a difference in some regression tests. The \after" version had some new warnings that weren't in the "before" version. After further investigation it turned out that displaying the warnings was correct and that the "before" version was unsound. This soundness...

Read More

Just a few more digits, please
Pascal Cuoq on 18 November 2011

Introduction: of Spivak pronouns In this post, I really let fly the Spivak pronouns. They are not used for the first time in this blog or in documentation but they are abused here. I have no serious justification for this sudden peak. I have a couple of unserious ones: I...

Read More

Analyzing single-precision floating-point constants
Pascal Cuoq on 14 November 2011

The previous post on this blog points out how subtle just floating-point constants can be. In a previous previous post exactly one year ago I was already alluding to these difficulties in the context of Frama-C's front-end. Programming a code analyzer that can answer question 5 How should the program...

Read More

Floating-point quiz
Pascal Cuoq on 8 November 2011

Here is a little quiz you can use to test your C floating-point expertise. I have tried to write the examples below so that the results do not depend too much on the platform and compiler. This is theoretically impossible since C99 does not mandate IEEE 754 floating-point semantics, but...

Read More

What functions does a function use: option -users
Pascal Cuoq on 5 November 2011

Exploring unfamiliar code Sometimes, one finds oneself in the situation of exploring unfamiliar code. In these circumstances, it is sometimes useful to know which functions a function f() uses. This sounds like something that can be computed from the callgraph, and there exists plenty of tools out there that can...

Read More