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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
---
layout: post
author: Pascal Cuoq
date: 2011-04-21 10:56 +0200
categories: value
format: xhtml
title: "List of the ways Frama_C_dump_each() is better than printf()"
summary:
---
{% raw %}
<p>In <a href="/index.php?post/2011/03/01/Interpretation-speed" hreflang="en">an older post</a> I recommended that the value analysis be launched on existing unit and integration tests.</p>
<p>One advantage of using a completely unrolled analysis as compared to traditional compilation-execution is that the "execution" then takes place in an environment we have complete control of. Let us say there is a strange behavior in a large integration test that we are trying to investigate. First running the test inside the value analysis we can make sure the strange behavior is not caused by a buffer overflow or similar treat of the C language. In addition where we would insert calls to <code>printf()</code> in order to get a trace of the values of some variables as some well-chosen points in the program we can use <code>Frama_C_dump_each()</code>.</p>
<p>For instance in the program below something strange seems to be happening inside function <code>f()</code> so we insert a call to <code>Frama_C_dump_each()</code> in a strategic location there.</p>
<pre>int x a;
int y=2;
int *p *q;
union { int i ; float f ; } u;
void f(void)
{
int lf = 5;
a = y + 2;
{
int lblock1 = 7;
p = &lblock1;
}
{
int lblock2;
q = &lblock2;
Frama_C_dump_each();
}
return;
}
main(){
int lmain = 3;
u.f = 1.5;
f();
return 0;
}
</pre>
<p>Launching <code>frama-c -val -slevel 5000 t.c</code> we get:</p>
<pre>[value] DUMPING STATE of file t.c line 16
x ∈ {0; }
a ∈ {4; }
y ∈ {2; }
p ∈ {{}} or ESCAPINGADDR
q ∈ {{ &lblock2 ;}}
u{.i; .f; } ∈ 1.5
lf ∈ {5; }
lmain ∈ {3; }
=END OF DUMP==
</pre>
<p>Below is a list of advantages of <code>Frama_C_dump_each()</code> over <code>printf()</code>. Am I forgetting some? Does GDB provide comparable features where applicable? (I must admit I haven't used GDB in a long time)</p>
<ul>
<li>By inserting a single statement in the program you get a log of the entire state including variables that are out of scope for reason of being static to another compilation unit or for reason of being local variables of a caller. All the variables that can influence the remainder of the execution are shown.</li>
<li><code>Frama_C_dump_each()</code> does not show uninitialized variable as appearing to have a value. For instance <code>lblock2</code> above is not show as containing <code>7</code> which is what <code>printf()</code> might have shown. Or <code>982475</code>.</li>
<li>Similarly the value of dangling pointers (pointers to stack variables that have ceased to exist) is shown as <code>ESCAPINGADDR</code> not as the address of some other variable that happens to occupy the same place in the stack. In the example above <code>printf()</code> might have shown <code>p</code> as pointing to <code>lblock2</code> or some other seemingly valid location in the stack.</li>
<li>With <code>Frama_C_dump_each()</code> addresses are shown in a symbolic form such as <code>{{ &lblock2 ;}}</code> for variable <code>q</code> in the example instead of some arbitrary address where <code>lblock2</code> happens to be located.</li>
<li>Contents of an union are shown using the type that was used to write there. In the example union <code>u</code> is shown as having received the floating-point value <code>1.5</code>. Using <code>printf()</code> we would have to choose between displaying <code>u.i</code> and <code>u.f</code> and if we chose the former the value would be hard to recognize for what it is.</li>
</ul>
<p>The one disadvantage is that this only works for executions that the value analysis is able to capture precisely. This means no recursion and no bitwise xor on the values of pointers.</p>
{% endraw %}