2

我正在尝试在 printf 调用中对以下程序进行切片：

#include <stdlib.h>
#include <stdio.h>

int main(int argc, char **argv) {

  if (argc < 3) return 1;

  int x = atoi(argv[1]);
  int y = atoi(argv[2]);

  printf("%d %d\n", x, y);

  return 0;
}

但是，价值分析插件会给出以下消息：

foo.c:9:[value] 函数调用表达式参数 (char const ) (argv + 2)的评估中的非终止，

切片的程序是空的！这是 Frama-C 中的错误/功能吗？还是我做错了什么？

这是一个完整的跟踪：

$ frama-c -slice-calls printf foo.c -then-on 'Slicing export' -print
[slicing] slicing requests in progress...
[kernel] preprocessing with "gcc -C -E -I.  foo.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
foo.c:8:[kernel] warning: out of bounds read. assert \valid(argv+1);
[value] computing for function atoi <- main.
        Called from foo.c:8.
[kernel] warning: No code for function atoi, default assigns generated
[value] Done for function atoi
foo.c:9:[kernel] warning: out of bounds read. assert \valid(argv+2);
foo.c:9:[value] Non-termination in evaluation of function call expression argument
        (char const *)*(argv + 2)
[value] Recording results for main
[value] done for function main
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[slicing] exporting project to 'Slicing export'...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
4

1 回答 1

2

参见价值分析手册中的5.2.3 不完整应用的分析：

对于指针类型的变量，分析器无法猜测是否应该假定指针指向单个元素或指向数组的开头——或者实际上是数组的中间，这意味着对该指针取负偏移量是合法的。默认情况下，假定指针类型指向由两个元素组成的数组的开头。这个数字可以用 option 改变-context-width。示例：如果入口点的原型是void main(int *t)，则分析器假定t指向数组int S_t[2]。

这同样适用于程序函数的argv参数main()。构建一个正确的指针数组，您希望它们与main()实践中的参数相对应，如手册中其他地方所述（例如 main_2.c 第 23 页）。如果您只想验证或分割您的程序以获得 0 .. 1000 范围内的格式良好的整数，您可以在分配/*@ assert 0 <= x <= 1000 ; */后插入程序中。x

[内核] 警告：没有函数 atoi 的代码，生成的默认分配

您还应该阅读同一手册中的2.3.3 缺失功能。告诉你，先看说明书，以后再尝试使用价值分析和切片插件。对于当今的一款软件来说，这是一个陡峭的学习曲线，但这正是它的实际使用方式。

无论如何，应该为分析器遇到的所有功能提供实现或最小规范。Frama-C 的最新版本在 share/libc 中包含一些非常好的规范，用于许多标准功能，它们可能已安装在您计算机上的 /usr/local/lib/Frama-C/libc 中。

于 2014-05-21T18:11:50.750 回答