Tag Archives: value

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

Checking for overflows, revisited once
Pascal Cuoq on 12 February 2012

I do not have any solution I am 100% happy with to the overflow dilemma in the previous post. Here is one of the solutions that does not make me 100% happy. The first (partial) solution is: program so that overflows correspond exactly to unwanted circumstances (and then it becomes...

Read More

Using the Rte and value analysis plug-ins to detect overflows
Pascal Cuoq on 4 February 2012

This post is another of the methodological cheat cards that made up much of this blog at its beginnings, before I decided that controversial comparisons between static analyzers were more fun to write. The problem: detecting semantic coding rules transgressions By default, Frama-C's value analysis does not warn about integer...

Read More

Checking for overflows operation by operation
Pascal Cuoq on 20 January 2012

My colleague Bernard Botella pointed out an interesting example in an offline discussion following the last quiz. The setup Consider the snippet: int s; unsigned u1 u2; ... s = u1 - u2; The programmer's intention with the assignment is to compute in variable s of type int the mathematical...

Read More

Csmith testing again
Pascal Cuoq on 16 January 2012

My presentation Friday at the U3CAT meeting was on the topic of Frama-C Csmith testing. Several posts in this blog already describe facets of this work (it has its own tag). Yet another angle can be found in this short article draft. Said draft by the way will soon need...

Read More