Frama-C: отображать стеки вызовов в выходных данных командной строки

Question

При использовании плагина анализа значений можно использовать графический интерфейс для отображения значений переменной в заданном месте программы (используя вкладку «Значения»).Значения, показанные на этой вкладке, включают стек вызовов, соответствующий определенному значению.Например:

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

В командной строке можно отобразить значения переменной, когда анализ достигает местоположения программы, используя Frama_C_show_each(var).Однако соответствующий стек вызовов не отображается.

Существует ли способ сообщить Frama-C о выводе стека вызовов в заданном месте программы для получения информации в форме (callstack, значения), как в графическом интерфейсе пользователя??

Заранее большое спасибо за любые указатели.

Answer 1

Плагин Eva (прежний Value analysis ) имеет возможность печатать стеки вызовов:

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

Этот, как и другие параметры Eva, доступен через frama-c -value-helpили frama-c -value-h.

В противном случае этот вопрос содержит пример сценария, который в сочетании с Db.Value.get_stmt_state_callstack должен позволить создать собственный способ печати нужной информации.