diff --git a/src/plugins/variadic/tests/defined/oracle/simple.0.res.oracle b/src/plugins/variadic/tests/defined/oracle/simple.0.res.oracle index d682b185f8e6766bf5acd7d25d211ac7cc35ba8d..c1ce928d7fe1ea7d1d6ec46b04f9b256963902b5 100644 --- a/src/plugins/variadic/tests/defined/oracle/simple.0.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/simple.0.res.oracle @@ -1,5 +1,5 @@ -[variadic] simple.c:9: Declaration of variadic function sum. -[variadic] simple.c:24: Generic translation of call to variadic function. +[variadic] simple.c:19: Declaration of variadic function sum. +[variadic] simple.c:34: Generic translation of call to variadic function. [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed @@ -12,7 +12,7 @@ [eva:final-states] Values at end of function main: /* Generated by Frama-C */ -#include "stdarg.h" +typedef void * const *va_list; /*@ requires n ≥ 0; */ int sum(int n, void * const *__va_params) { diff --git a/src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle b/src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle index 7b5221cf83de9df7862c7d97e175b5b68ddb6eba..c1ce928d7fe1ea7d1d6ec46b04f9b256963902b5 100644 --- a/src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle @@ -1,5 +1,5 @@ -[variadic] simple.c:9: Declaration of variadic function sum. -[variadic] simple.c:24: Generic translation of call to variadic function. +[variadic] simple.c:19: Declaration of variadic function sum. +[variadic] simple.c:34: Generic translation of call to variadic function. [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed @@ -12,8 +12,7 @@ [eva:final-states] Values at end of function main: /* Generated by Frama-C */ -typedef void * const *__gnuc_va_list; -typedef __gnuc_va_list va_list; +typedef void * const *va_list; /*@ requires n ≥ 0; */ int sum(int n, void * const *__va_params) { diff --git a/src/plugins/variadic/tests/defined/simple.c b/src/plugins/variadic/tests/defined/simple.c index b2346a3f09cadb78412a84f82bd1deca74232c59..617d61e43804845cb0e6629c7808156cada69cea 100644 --- a/src/plugins/variadic/tests/defined/simple.c +++ b/src/plugins/variadic/tests/defined/simple.c @@ -1,10 +1,20 @@ /* run.config -STDOPT: -STDOPT: #"-no-frama-c-stdlib -no-pp-annot" +STDOPT: #"-c11" +STDOPT: #"-no-frama-c-stdlib -no-pp-annot -c11" */ +/* The defines and typedefs below avoid issues with Musl: without them, + pretty-printing 'va_list' results in `typedef __gnuc_va_list va_list`, but + only on GNU libc-based systems (and not on Alpine Linux, which is based on + musl). */ +#define __GNUC_VA_LIST +#define __va_list__ +typedef void *__builtin_va_list; +typedef __builtin_va_list va_list; #include <stdarg.h> + + /*@ requires n>= 0; */ int sum(int n, ...){ int ret = 0;