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

Question

Я хочу нарезать неиспользуемые переменные, которые отображаются с frama-c. Но я понятия не имею, какую командную строку я должен написать, чтобы разделить все неиспользуемые переменные одной командной строкой

Last login: Thu Nov  9 20:48:42 on ttys000
Recep-MacBook-Pro:~ recepinanir$ cd desktop
Recep-MacBook-Pro:desktop recepinanir$ cat hw.c
#include <stdio.h>

int main()
{
    int x= 10;
    int y= 24;
    int z;

  printf("Hello World\n");

  return 0;
}

Recep-MacBook-Pro:desktop recepinanir$ clang hw.c
Recep-MacBook-Pro:desktop recepinanir$ ./a.out
Hello World
Recep-MacBook-Pro:desktop recepinanir$ clang -Wall hw.c -o result
hw.c:5:9: warning: unused variable 'x' [-Wunused-variable]
    int x= 10;
        ^
hw.c:6:9: warning: unused variable 'y' [-Wunused-variable]
    int y= 24;
        ^
hw.c:7:9: warning: unused variable 'z' [-Wunused-variable]
    int z;
        ^
3 warnings generated.
Recep-MacBook-Pro:desktop recepinanir$ 

Answer 1

Как упоминалось на https://frama-c.com/slicing.html, нарезка всегда является относительным некоторым критерием, и цель состоит в том, чтобы создать программу, меньшую по сравнению с исходной, и демонстрирующую то же поведение по отношению к критерию., Сам плагин Slicing предоставляет несколько способов построения таких критериев, но, похоже, вы заинтересованы в результате использования плагина Sparecode ( https://frama-c.com/sparecode.html): это специализированная версия нарезка, где критерием является состояние программы в конце точки входа вашего анализа (т.е. main в твоем случае). Другими словами, Sparecode удалит все, что не влияет на конечный результат анализируемого кода. В твоем случае, frama-c -sparecode-analysis hw.c дает следующий результат (обратите внимание, что вызов printf был изменен плагином Variadic, и его аргумент не считается полезным для конечного состояния main. Если это проблема, вам нужно предоставить более специализированные выходные функции со спецификацией ACSL, указывающей, что они влияют на некоторую глобальную переменную)

/* Generated by Frama-C */
#include "stdio.h"
/*@ assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
             __fc_stdout->__fc_FILE_data;
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data;
 */
int printf_va_1(void);

int main(void)
{
  int __retres;
  printf_va_1();
 __retres = 0;
 return __retres;
}

Наконец, обратите внимание, что в общем случае Slicing (следовательно, Sparecode) дает избыточную приближение: он удалит только те операторы, для которых он уверен, что они не влияют на критерий.