List of the ways Frama_C_dump_each() is better than printf()

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)

• 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.
• 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.
• Similarly the value of dangling pointers (pointers to stack variables that have ceased to exist) is shown as 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.
• With 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.
• Contents of an union are shown using the type that was used to write there. In the example union 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.