--- 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 %}
In an older post I recommended that the value analysis be launched on existing unit and integration tests.
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 printf()
in order to get a trace of the values of some variables as some well-chosen points in the program we can use Frama_C_dump_each()
.
For instance in the program below something strange seems to be happening inside function f()
so we insert a call to Frama_C_dump_each()
in a strategic location there.
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; }
Launching frama-c -val -slevel 5000 t.c
we get:
[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==
Below is a list of advantages of Frama_C_dump_each()
over printf()
. Am I forgetting some? Does GDB provide comparable features where applicable? (I must admit I haven't used GDB in a long time)
Frama_C_dump_each()
does not show uninitialized variable as appearing to have a value. For instance lblock2
above is not show as containing 7
which is what printf()
might have shown. Or 982475
.ESCAPINGADDR
not as the address of some other variable that happens to occupy the same place in the stack. In the example above printf()
might have shown p
as pointing to lblock2
or some other seemingly valid location in the stack.Frama_C_dump_each()
addresses are shown in a symbolic form such as {{ &lblock2 ;}}
for variable q
in the example instead of some arbitrary address where lblock2
happens to be located.u
is shown as having received the floating-point value 1.5
. Using printf()
we would have to choose between displaying u.i
and u.f
and if we chose the former the value would be hard to recognize for what it is.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.
{% endraw %}