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

Question

Currently, I am using Frama-C version 19, and struggling with variadic arguments. For example)

  #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;
 }

I am getting warning of '[eva:alarm] main.c:6: Warning: out of bounds read. assert \valid_read(args)'. Is there any way to write pre-condition for args in above code? I tried to cast to void and int, but did not help much. Many thanks for the help in advance.

BRs, Jaesu Yu

Answer 1

Your example is correct, and the warning is unrelated to variadic functions. Simply increasing a bit the precision of the analysis is enough to allow Eva to separately explore each loop iteration and obtain a precise result. For instance:

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

When running with this bit of extra precision, I get no warnings.

Longer explanation

By default, Eva will limit the exploration of all branches (and loop iterations) in the program, using some heuristics to decide when to apply widening (fast convergence) to avoid spending too much time in the analysis. This is the standard approach in abstract interpretation-based analyses.

Eva is highly parametrizable, with several options to adjust the trade-off between speed and precision of the analysis. For small programs such as yours, you can increase the precision (it goes up to 11) without issues. For larger programs (several thousands lines of code, or more), more careful adjusting may be needed.

If you encounter similar issues in the future, especially inside loops or code with lots of branching, one of the first approaches you should try is to increase the precision, if the analysis time remains reasonable.