c - Frama-C 是否捕获了读取未初始化堆栈变量的 UB？

Question

我正在探索 Frama-C 并尝试了这个示例，根据手册(第 83 页)应该处理它(CWE-457)，以及 RTE 手册 2.7(整数有陷阱表示吗？ http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm )应该被覆盖吗？

/*@ assigns \nothing; @*/
int f() {
  int a;
  return a;
}

/*@ assigns \nothing; @*/
int main() {
    if (f() < 0) {
        return 0;
    } else {
        return 1;
    }
}                                                                                                                                                

#include<stdio.h>

/*@ assigns \nothing; @*/
char f() {
  char a;
  return a;
} 
                                                                                                                                                          
/*@ assigns \nothing; @*/
int main() {
  char s[2];
  s[0] = f();
  s[1] = '\0';
  puts(s);
  return 0;
} 

但是，当我运行这些示例时，它们似乎通过了。这是预期的行为吗？

Answer 1

正如 manual of the RTE plugin 中提到的(诚然不是以非常突出的方式) ，在第 20 页的表 3.2 中，生成初始化相关断言的函数集默认为空。主要原因是它可能会生成大量断言(基本上每次使用未显式初始化的局部变量时)，并且用户对它们的兴趣往往不如例如断言。无效的指针取消引用或算术溢出。

如果要为所有函数生成它们，则需要在 Frama-C 命令行上使用 -rte-initialized @all，如下所示:frama-c -wp - wp-rte -rte-initialized @all file.c。您可以在手册的第 2.7 节中找到有关 RTE 处理初始化断言的更多信息。