Frama-c值分析中的无效位置

Question

我正在尝试使用值分析来分析类似于以下内容的一些程序：

int main(int argc, char **argv){
  char *argv0 = argv[0];
  char x = argv0[1];
  char y = argv0[2];
  return 0;
}

标准化和分析后的程序如下所示：

int main(int argc, char **argv){
  int __retres;
  char *argv0;
  char x;
  char y;
  /*@ assert Value: mem_access: \valid_read(argv + 0); */
  argv0 = *(argv + 0);
  /*@ assert Value: mem_access: \valid_read(argv0 + 1); */
  x = *(argv0 + 1);
  /*@ assert Value: mem_access: \valid_read(argv0 + 2); */
  y = *(argv0 + 2);
  __retres = 0;
  return __retres;
}

其中前两个断言的状态是'unknown'，第三个断言的状态是'invalid'。此外，值分析告诉我 *(argv0 + 2) 是一个无效位置，并将它之后的所有代码标记为已死。

我想了解为什么最后一个断言无效（而不是前两个）以及为什么 *(argv0 + 2) 是一个无效位置。

我正在使用 Frama-c Silicon-20161101

Answer 1

感谢 anol 的评论，我能够在 Value Analysis (http://frama-c.com/download/frama-c-value-analysis.pdf) 的用户手册中找到相关部分。

摘录如下：

5.2.4 Tweaking the automatic generation of initial values (p58)

(...)

For a variable of a pointer type, there is no way for the analyzer to guess whether the pointer should be assumed to be pointing to a single element or to be pointing at the beginning of an array — or indeed, in the middle of an array, which would mean that it is legal to take negative offsets of this pointer.

By default, a pointer type is assumed to point at the beginning of an array of two elements. This number can be changed with option -context-width.

Frama-c值分析中的无效位置

Invalid location in Frama-c value analysis

frama-c