Tag Archives: rte

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