使用Frama-c对C代码进行切片
使用Frama-c对C代码进行切片
提问于 2017-11-10 02:09:51
我想对未使用的变量进行切片，这些变量用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$ 回答 1
Stack Overflow用户
发布于 2017-11-10 16:01:07
正如在https://frama-c.com/slicing.html上提到的，切片总是相对于某些标准而言的，目标是产生一个比原始程序更小的程序，同时呈现与该标准相同的行为。切片插件本身提供了几种构建此类标准的方法，但您似乎对Sparecode插件(https://frama-c.com/sparecode.html)的结果感兴趣:这是切片的专用版本，其中标准是分析入口点(即您的案例中的main )结束时的程序状态。换句话说，Sparecode将删除与所分析代码的最终结果无关的所有内容。在您的示例中，frama-c -sparecode-analysis hw.c给出了以下结果(请注意，对printf的调用已被可变插件修改，并且其参数对于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;
}最后，请注意，在一般情况下，切片(因此是Sparecode)提供了过度近似:它只会删除那些确定它们对标准没有影响的语句。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/47208799
复制相关文章
相似问题
腾讯云开发者
