Можно ли получить обратный динамический срез в Frama-C?

Question

Я получаю обратную часть от Frama-c, но выглядит как статическая часть, а не как динамическая часть.

Есть ли конкретная опция в frama-c для получения динамического обратного среза?

Answer 1

Согласно Википедии,

Динамический фрагмент содержит все операторы, которые фактически влияют на значение переменной в программной точке для конкретного выполнения программы, а не все операторы, которые могли повлиять на значение переменной в программной точке для любого произвольного выполнения программы.

Плагин нарезки Frama-C обусловлен значениями из плагина анализа значений, которые берут на себя веру, чтобы представить все значения, которые происходят для выполнения в наборе интересующих исполнений. Чтобы настроить плагин среза Frama-C для динамического среза, вам просто нужно, чтобы анализ значений соответствовал одному выполнению. Используя main функция без входов, нет volatile переменные, без вызова неизвестных функций и передачи опции -slevel 999999999 в frama-c должен заставить анализ значений вести себя как интерпретатор C при единственном выполнении программы по вашему выбору, как описано в этом предыдущем ответе на другой вопрос, в этом посте в блоге и в этой статье.