Нарезка с помощью Frama-c

Question

Я установил frama-c с opam на свои MacO. Мне нужно нарезать Hello World вручную. Я имею в виду не с Gui. Я искал в интернете, но я не мог понять, как это сделать. Мой английский недостаточно хорош. Так может кто-нибудь помочь мне нарезать HelloWorld.c?

Answer 1

Чтобы запустить срез Frama-C из командной строки, у вас должен быть файл C, который анализирует, и критерий среза (код возврата, доступ к глобальной переменной, оператор и т. Д.). Различные доступные критерии описаны по адресу http://frama-c.com/slicing.html.

Кроме того, если вы хотите нарезать, например, оператор, вам придется использовать нарезку прагм со следующим синтаксисом:

/*@ slice pragma stmt; */
    Preserves the effects of the next statement. 
/*@ slice pragma expr e; */
    Preserves the value of the ACSL expression e at this control-flow point.