From ba00b7b7c4c5d3ab496f74b6183462ecd714af77 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 1 Jun 2022 17:19:49 +0200
Subject: [PATCH] [Variadic] avoid musl-related test differences
---
.../tests/defined/oracle/simple.0.res.oracle | 6 +++---
.../tests/defined/oracle/simple.1.res.oracle | 7 +++----
src/plugins/variadic/tests/defined/simple.c | 14 ++++++++++++--
3 files changed, 18 insertions(+), 9 deletions(-)
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 d682b185f8e..c1ce928d7fe 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 7b5221cf83d..c1ce928d7fe 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 b2346a3f09c..617d61e4380 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;
--
GitLab