Frama-c:如何用va_list和va_arg来证明可变参数的合理性?

Question

目前，我正在使用Frama-C版本19，并且正在努力解决可变参数。例如(

#include <stdarg.h>
#include <stddef.h>
void vars2(int n, va_list args) {
for (size_t i = 0; i < n; ++i) {
int tmp = va_arg(args, int);
}
};
void vars(int n, ...) {
va_list args;
va_start(args, n);
vars2(n, args);
va_end(args);
};
int main(void) {
vars(5, 1, 2, 3, 4, 5);
return 0;
}

我收到"[eva：alarm] main.c：6：警告：越界读取。 断言 \valid_read(args("。有没有办法在上面的代码中为 args 编写前提条件？我试图投射到虚空和内，但没有多大帮助。非常感谢提前提供的帮助。

无线电通信量， 于宰苏

Answer 1

您的示例是正确的，并且警告与可变参数函数无关。只需稍微提高分析精度，Eva就可以单独探索每个循环迭代并获得精确的结果。例如：

frama-c -eva -eva-precision 1 file.c

当以这种额外的精度运行时，我没有得到任何警告。

更长的解释

默认情况下，Eva将限制程序中所有分支(和循环迭代(的探索，使用一些启发式方法来决定何时应用加宽(快速收敛(，以避免在分析中花费太多时间。这是基于抽象解释的分析中的标准方法。

Eva具有高度参数化的特点，有多种选择可用于调整分析速度和精度之间的权衡。对于像您这样的小程序，您可以毫无问题地提高精度(最高可达 11(。对于较大的程序(数千行代码或更多(，可能需要更仔细的调整。

如果将来遇到类似的问题，尤其是在循环或具有大量分支的代码内部，如果分析时间仍然合理，您应该尝试的第一种方法是提高精度。