Skip to content
Snippets Groups Projects
Commit ba00b7b7 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Variadic] avoid musl-related test differences

parent a1f448a6
No related branches found
No related tags found
No related merge requests found
[variadic] simple.c:9: Declaration of variadic function sum. [variadic] simple.c:19: Declaration of variadic function sum.
[variadic] simple.c:24: Generic translation of call to variadic function. [variadic] simple.c:34: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main [eva] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
/* Generated by Frama-C */ /* Generated by Frama-C */
#include "stdarg.h" typedef void * const *va_list;
/*@ requires n ≥ 0; */ /*@ requires n ≥ 0; */
int sum(int n, void * const *__va_params) int sum(int n, void * const *__va_params)
{ {
......
[variadic] simple.c:9: Declaration of variadic function sum. [variadic] simple.c:19: Declaration of variadic function sum.
[variadic] simple.c:24: Generic translation of call to variadic function. [variadic] simple.c:34: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main [eva] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
[eva] Initial state computed [eva] Initial state computed
...@@ -12,8 +12,7 @@ ...@@ -12,8 +12,7 @@
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
/* Generated by Frama-C */ /* Generated by Frama-C */
typedef void * const *__gnuc_va_list; typedef void * const *va_list;
typedef __gnuc_va_list va_list;
/*@ requires n ≥ 0; */ /*@ requires n ≥ 0; */
int sum(int n, void * const *__va_params) int sum(int n, void * const *__va_params)
{ {
......
/* run.config /* run.config
STDOPT: STDOPT: #"-c11"
STDOPT: #"-no-frama-c-stdlib -no-pp-annot" 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> #include <stdarg.h>
/*@ requires n>= 0; */ /*@ requires n>= 0; */
int sum(int n, ...){ int sum(int n, ...){
int ret = 0; int ret = 0;
......
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