Variadic

Overview

The Variadic plug-in (enabled by default) performs the translation of calls to variadic functions into calls to semantically equivalent, but non-variadic functions.

Variadic enables other plug-ins to automatically handle programs containing variadic calls, without having to implement specific behavior to handle them.

It also performs some conformance checks in variadic function calls, emitting warnings when possible violations of the C standard are detected.

Finally, Variadic generates function prototypes with ACSL specifications for each variadic call. These specifications ensure that required preconditions are verified, and allow other analyses to reason about calls to these variadic functions.

Quick Start

The plug-in is automatically enabled by default and performs its code transformation before the analyses specified in the command-line. The result can be output via the kernel option -print. It can also be directly used by other plug-ins.

Example

Example input:

#include <stdio.h>
void main() {
  int n = 5;
  printf("%d, %*s", 42, n, "hello");
}

Example output:

/* Generated by Frama-C */
#include <stdio.h>
/*@ requires valid_read_string(format);
    requires valid_read_string(param2);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            (indirect: __fc_stdout->__fc_FILE_data),
            (indirect: *(format + (0 ..))), (indirect: *(param2 + (0 ..))),
            (indirect: param1), (indirect: param0);
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
            *(param2 + (0 ..)), param1, param0;
 */
int printf_va_1(char const * __restrict format, int param0, int param1,
                char *param2);

void main(void)
{
  int n = 5;
  printf_va_1("%d, %*s",42,n,(char *)"hello");
  return;
}

The plug-in can be made more strict via option -variadic-strict, which enables checking non-portable implicit casts in calls of standard variadic functions.

If necessary, the Variadic plug-in can be disabled via option -variadic-no-translation.

Technical Notes

Maturity: strong
Calls to standard variadic functions such as printf and scanf with non-static format arguments are not currently supported. For instance, the following call is not translated by the plug-in:
```
  #include <stdio.h>
  void f(int n) {
    printf(n &lt; 2 ?
    "%d packet is available" :
    "%d packets are available", n);
  }
```

Also, unless option -print-libc is enabled, the output produced by Variadic, in particular when using macros va_list, va_arg, etc, is not guaranteed to be parsable. Using -print-libc avoids this issue.