--- layout: plugin title: Variadic description: Variadic simplifies variadic functions for other plug-ins. key: code ---
Overview

The Variadic plug-in (distributed with Frama-C and 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.

Maturity: Mature

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),
	      __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
	      *(param2 + (0 ..)), param1, 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 *format, int param0,
		int param2, char *param3);

	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

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.

Documentation

Information about the plug-in is available via its help option:

frama-c -variadic-help

If you want more detailed information about this plug-in, please contact us.

Variadic has no specific user manual; its usage is presented in the Frama-C user manual