Skip to content
Snippets Groups Projects
Commit 5bf545f8 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] add test checking that variadic does generate fresh names

parent a4bd50ce
No related branches found
No related tags found
No related merge requests found
[kernel] Parsing variadic_fresh_names.c (with preprocessing)
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), param0;
*/
int fprintf_va_1(FILE * restrict stream, char const * restrict format,
int param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), param0;
*/
int fprintf_va_2(FILE * restrict stream, char const * restrict format,
int param0);
void main(void)
{
fprintf(__fc_stderr,"%d ",42); /* fprintf_va_2 */
return;
}
/* run.config
PLUGIN: variadic
STDOPT:
*/
#include "stdio.h"
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..))), (indirect: param0);
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..))), param0;
*/
int fprintf_va_1(FILE * restrict stream, char const * restrict format,
int param0);
void main(void)
{
fprintf(__fc_stderr,"%d ",42); /* fprintf_va_1 */
return;
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment