--- layout: post author: Pascal Cuoq date: 2012-03-27 11:45 +0200 categories: nitrogen value format: xhtml title: "Overflow alarms vs informative messages about 2's complement" summary: --- {% raw %}
A privately sent question may deserve a quick blog post.
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 that the program is flirting with the limits of 32-bit 2's complement integers. Frama-C's value analysis with default options finds the following to say:
$ frama-c -val share/builtin.c o.c ... o.c:6:[value] warning: 2's complement assumed for overflow o.c:6:[value] assigning non deterministic value for the first time [value] DUMPING STATE of file o.c line 7 x ∈ [0..2000000000] y ∈ {1000000000} s ∈ [--..--]
There is an option, -val-signed-overflow-alarms
, to change the behavior of the value analysis with respect to integer overflows:
$ frama-c -val -val-signed-overflow-alarms share/builtin.c o.c ... o.c:6:[kernel] warning: Signed overflow. assert x+y ≤ 2147483647LL; o.c:6:[value] assigning non deterministic value for the first time [value] DUMPING STATE of file o.c line 7 x ∈ [0..2000000000] y ∈ {1000000000} s ∈ [1000000000..2147483647]
The warning with the first command was introduced in Nitrogen, and this post therefore is in a way part of the series describing new features in Nitrogen.
The new warning, “2's complement assumed for overflow”, is emitted in exactly the same circumstances the alarm “assert x+y ≤ 2147483647LL” would have been emitted if option -val-signed-overflow-alarms
had been used.
The question is whether the warnings obtained in each case, “2's complement assumed for overflow” and “Signed overflow. assert x+y ≤ 2147483647LL” respectively, mean the same thing. The answer is that no, they don't. The consequences of the differences between them can be seen in the values computed for variable s
after the overflow.
[-2147483648..-1294967296] ∪ [1000000000..2147483647]
but since the value analysis can only represent large sets of integers as a single interval the end result is that all int
values appear to be possible values for variable s
.s
is guaranteed to be in the range [1000000000..2147483647]
. This is a subset of the values that are possible with 2's complement addition. Now the value analysis also reserves the right to reduce after the alarm the values for variable x
to the range [0..1147483647]
since these are the only values that do not cause an undefined overflow. It does not take advantage of this information at this level for now but a future version will. The reasoning here is the same as the reasoning in Q1 and Q2 in the Frequently Asked Questions section of the manual.It may seem strange that in the second case the value analysis does not affirm more strongly that there is a definite problem with some of the values in the user-specified
Frama_C_interval(0 2000000000)
range for variablex
but that's not what it is optimized for. It is optimized for verifying that there aren't any issues not so much for reliably telling the user what original inputs cause the issues. User expertise or alternative techniques must take up from there. Think of the range[0..2000000000]
forx
as the result of previous computations without it being known whether the interval is so wide because the values can really happen with user-specified inputs or because of earlier over-approximations.
Stéphane Duprat Florent Kirchner and Philippe Herrmann proofread this post.
{% endraw %}