Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
---
layout: post
author: Pascal Cuoq
date: 2011-07-26 10:55 +0200
categories: conversions-and-promotions facetious-colleagues value
format: xhtml
title: "Fun with usual arithmetic conversions"
summary:
---
{% raw %}
<p>A facetious colleague reports the following program as a bug:</p>
<pre>int main () {
signed char c=0;
while(1) c++;
return 0;
}
</pre>
<p>The commandline <code>frama-c -val -val-signed-overflow-alarms charpp.c</code>, he says,
does not emit any alarm for the <code>c++;</code> instruction.</p>
<p>Indeed, the <code>c++;</code> above is equivalent to <code>c = (signed char) ((int)c + 1);</code>.</p>
<p>If the implementation-defined(6.3.1.3 §3) conversions from <code>int</code> to <code>signed char</code> are assumed to give
the expected modulo results, this instruction never displays undefined behavior. The really dangerous operation,
signed addition, takes place between arguments of type <code>int</code> and returns an <code>int</code>.
Thus, in this particular program and for the default x86_32 target architecture, the result of the addition is
always representable in the result type.</p> <p>A facetious colleague reports the following program as a bug:</p>
<pre>int main () {
signed char c=0;
while(1) c++;
return 0;
}
</pre>
<p>The commandline <code>frama-c -val -val-signed-overflow-alarms charpp.c</code>, he says,
does not emit any alarm for the <code>c++;</code> instruction.</p>
<p>Indeed, the <code>c++;</code> above is equivalent to <code>c = (signed char) ((int)c + 1);</code>.</p>
<p>If the implementation-defined(6.3.1.3 §3) conversions from <code>int</code> to <code>signed char</code> are assumed to give
the expected modulo results, this instruction never displays undefined behavior. The really dangerous operation,
signed addition, takes place between arguments of type <code>int</code> and returns an <code>int</code>.
Thus, in this particular program and for the default x86_32 target architecture, the result of the addition is
always representable in the result type.</p>
{% endraw %}