使用 Frama-c 切片 C 代码答案

【问题标题】：Slicing a C code with Frama-c使用 Frama-c 切片 C 代码
【发布时间】：2017-11-09 18:09:50
【问题描述】：

我想对用 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$

【问题讨论】：

标签： clang frama-c program-slicing

【解决方案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）给出了一个过度近似：它只会删除确定它们对标准没有影响的语句。

【讨论】：