CC: Provide stdarg.h as a compiler builtin.

dios/include/stdarg.h

-/* 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

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" )

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() { }

divine/cc/stdarg.h

+// -*- 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