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 编写前置条件？我试图投射到 void 和 int，但没有太大帮助。非常感谢您的提前帮助。

BR，于再秀

Answer 1

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

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

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

更长的解释

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

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

如果您以后遇到类似问题，尤其是内部循环或包含大量分支的代码，您应该尝试的首要方法之一是提高精度，前提是分析时间保持合理。

Frama-c：如何用 va_list 和 va_arg 证明可变参数的合理性？

Frama-c: How to justify variadic argument with va_list and va_arg?

variadic-functions

specifications

frama-c

formal-verification

preconditions

更长的解释