3

When using the value analysis plug-in, one can use the GUI to display the values of a variable at a given program location (using the 'Values' tab). The values shown in this tab include the call stack corresponding to a particular value. E.g.:

fn1 -> fn2 -> fn3 | {values}
fn4 -> fn5 -> fn3 | {values}

On the command line, one can display the values of a variable when analysis reaches a program location by using Frama_C_show_each(var). However, the corresponding call stack is not displayed.

Is there a way to tell Frama-C to output the call stack at a given program location to obtain information of the form (callstack, values) as in the GUI?

Thanks a lot in advance for any pointers.

Sergio Feo
  • 292
  • 2
  • 7

1 Answers1

4

The Eva (former Value analysis) plug-in has an option to print callstacks:

-val-print-callstacks  When printing a message, also show the current call
                       stack (opposite option is -no-val-print-callstacks)

This, as well as other Eva options, is accessible via frama-c -value-help, or frama-c -value-h.

Otherwise, this question contains an example script which, combined with Db.Value.get_stmt_state_callstack, should allow crafting a custom way to print the desired information.

anol
  • 8,264
  • 3
  • 34
  • 78
  • Thanks a lot for your answer, this indeed works! Note that the stacks will be printed every time `Frama_C_show_each` is reached, or an assertion value is reported. – Sergio Feo Oct 01 '18 at 11:15