From 1cd200673d50b5282084204fe0de85cdeaef41df Mon Sep 17 00:00:00 2001
From: Zuzana Baranova <xbaranov@fi.muni.cz>
Date: Sun, 23 Jun 2019 21:36:14 +0000
Subject: [PATCH] CC: Provide stdarg.h as a compiler builtin.

---
 dios/include/stdarg.h | 27 --------------------------
 divine/CMakeLists.txt |  1 +
 divine/cc/cc1.cpp     |  7 ++++++-
 divine/cc/stdarg.h    | 44 +++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 51 insertions(+), 28 deletions(-)
 delete mode 100644 dios/include/stdarg.h
 create mode 100644 divine/cc/stdarg.h

diff --git a/dios/include/stdarg.h b/dios/include/stdarg.h
deleted file mode 100644
index 437a99c11..000000000
--- a/dios/include/stdarg.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/* Variable arguments <stdarg.h>
-
-   This file is part of the Public Domain C Library (PDCLib).
-   Permission is granted to use, modify, and / or redistribute at will.
-*/
-
-#ifndef _PDCLIB_STDARG_H
-#define _PDCLIB_STDARG_H _PDCLIB_STDARG_H
-#include "_PDCLIB/cdefs.h"
-#include "_PDCLIB/config.h"
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-typedef _PDCLIB_va_list va_list;
-
-#define va_arg( ap, type )    _PDCLIB_va_arg( ap, type )
-#define va_copy( dest, src )  _PDCLIB_va_copy( dest, src )
-#define va_end( ap )          _PDCLIB_va_end( ap )
-#define va_start( ap, parmN ) _PDCLIB_va_start( ap, parmN )
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
diff --git a/divine/CMakeLists.txt b/divine/CMakeLists.txt
index 59112f58d..a947b18d2 100644
--- a/divine/CMakeLists.txt
+++ b/divine/CMakeLists.txt
@@ -32,6 +32,7 @@ add_definitions( ${MPI_COMPILE_FLAGS} ${LLVM_COMPILE_FLAGS} )
 add_definitions( ${DIVINE_DEFINES} )
 
 stringify( cc ${divine_SOURCE_DIR}/divine/cc stddef.h )
+stringify( cc ${divine_SOURCE_DIR}/divine/cc stdarg.h )
 
 # add_library( divine-ss ${CPP_ss} )
 add_library( divine-ui ${CPP_ui} ${VERSION_FILE} "flags-generated.cpp" )
diff --git a/divine/cc/cc1.cpp b/divine/cc/cc1.cpp
index fe1335464..5d951fde8 100644
--- a/divine/cc/cc1.cpp
+++ b/divine/cc/cc1.cpp
@@ -32,7 +32,11 @@ DIVINE_UNRELAX_WARNINGS
 #include <divine/cc/cc1.hpp>
 #include <lart/divine/vaarg.h>
 
-namespace divine::str::cc { extern const std::string_view stddef_h; }
+namespace divine::str::cc
+{
+    extern const std::string_view stddef_h;
+    extern const std::string_view stdarg_h;
+}
 
 namespace divine::cc
 {
@@ -81,6 +85,7 @@ namespace divine::cc
             ctx.reset( new llvm::LLVMContext );
 
         mapVirtualFile( "/builtin/stddef.h", ::divine::str::cc::stddef_h );
+        mapVirtualFile( "/builtin/stdarg.h", ::divine::str::cc::stdarg_h );
     }
 
     CC1::~CC1() { }
diff --git a/divine/cc/stdarg.h b/divine/cc/stdarg.h
new file mode 100644
index 000000000..8af858d17
--- /dev/null
+++ b/divine/cc/stdarg.h
@@ -0,0 +1,44 @@
+// -*- mode: C++; indent-tabs-mode: nil; c-basic-offset: 4 -*-
+
+/*
+ * Permission to use, copy, modify, and distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+#ifndef _STDARG_H
+#define _STDARG_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+typedef __builtin_va_list va_list;
+
+  // this will be replaced by the va_arg instruction using LART
+#ifdef __cplusplus
+  void *__lart_llvm_va_arg( va_list va ) throw();
+  #define va_arg( ap, type ) (static_cast< type >( \
+        *reinterpret_cast< type * >(__lart_llvm_va_arg( (ap) ))))
+#else
+  void *__lart_llvm_va_arg( va_list va ) __attribute__((__nothrow__));
+  #define va_arg( ap, type ) ((type)(*(type *)__lart_llvm_va_arg( (ap) )))
+#endif
+
+#define va_copy( dest, src ) (__builtin_va_copy( (dest), (src) ))
+#define va_end( ap ) (__builtin_va_end( ap ) )
+#define va_start( ap, parmN ) (__builtin_va_start( (ap), (parmN) ))
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
-- 
GitLab