Skip to content
Snippets Groups Projects
Commit 6f2efbe1 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

[Variadic] Add a test about the conversion of va_arg results

parent 01491b56
No related branches found
No related tags found
No related merge requests found
[kernel:parser:decimal-float] va_arg_cast.c:17: Warning:
Floating-point constant 7.1 is not represented exactly. Will use 0x1.c666666666666p2.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[variadic] va_arg_cast.c:10: Declaration of variadic function c.
[variadic] va_arg_cast.c:17: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function b:
a ∈ {4619679907765970542}
ap ∈ {{ &__va_args[2] }}
[eva:final-states] Values at end of function c:
a ∈ {4619679907765970542}
ap ∈ {{ &__va_args[0] }}
[eva:final-states] Values at end of function main:
a ∈ {4619679907765970542}
/* Generated by Frama-C */
#include "stdarg.h"
long a;
void b(va_list ap)
{
long tmp;
a = (long)*((double *)*ap);
ap ++;
tmp = *((long *)*ap);
ap ++;
a += tmp;
return;
}
void c(int d, void * const *__va_params)
{
va_list ap;
ap = __va_params;
b(ap);
return;
}
void main(void)
{
{
double __va_arg0 = 8.1;
double __va_arg1 = 7.1;
void *__va_args[2] = {& __va_arg0, & __va_arg1};
c(0,(void * const *)(__va_args));
}
return;
}
#include <stdarg.h>
long a;
void b(va_list ap) {
a = va_arg(ap, double);
a += va_arg(ap, long);
}
void c(int d, ...) {
va_list ap;
va_start(ap, d);
b(ap);
}
void main() {
c(0, 8.1, 7.1);
}
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