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.
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.