Blog

Tag Archives: nitrogen

Overflow alarms vs informative messages about 2's complement
Pascal Cuoq on 27 March 2012

A privately sent question may deserve a quick blog post. Context The example is as below: int x, y, s; main(){ x = Frama_C_interval(0, 2000000000); y = 1000000000; s = x + y; Frama_C_dump_each(); } Sorry for all the zeroes. There are nine of them in each large constant, so...

Read More

Minimizing the number of alarms emitted by the value analysis
Pascal Cuoq on 12 March 2012

This blog post describes for the first time some options that became available in Nitrogen, continuing this series. This post also offers a benchmark but the results of this benchmark cannot be reproduced with Nitrogen. They should be reproducible with the next version of Frama-C. Alarms false alarms and redundant...

Read More

Formidable colleagues, patchlevels and new features in Nitrogen
Pascal Cuoq on 5 December 2011

My colleagues are formidable. Over the last few days, three of them fixed four bugs in my code. And one of the fixes was a simple, obviously correct fix for the bug previously discussed here. In celebration of these terrific colleagues here is a new patchset for Nitrogen 20111001 patchlevel...

Read More

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

Speaking of bug fixes, here is what a proper post-release patch looks like. This patch fixes five issues identified since Nitrogen was released. I have not tested the patch itself (I have not even tried applying it to the original tarball) — this is where you come in dear reader....

Read More

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