test for va_args

smowton · Sep 19, 2017 · 00cbad7 · 00cbad7
1 parent 0cec13d
commit 00cbad7
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 0 deletions.
diff --git a/regression/cbmc/va_list3/main.c b/regression/cbmc/va_list3/main.c
@@ -0,0 +1,29 @@
+#include <stdio.h> 
+#include <stdarg.h> 
+#include <assert.h> 
+
+void foo(int n, ...);
+
+int main()
+{
+  foo(1, 1u);
+  foo(2, 2l);
+  foo(3, 3.0);
+  return 0;
+}
+
+void foo(int n, ...)
+{
+  va_list vl;
+
+  va_start(vl,n);
+
+  switch(n)
+  {
+  case 1: assert(va_arg(vl, unsigned)==1); break;
+  case 2: assert(va_arg(vl, long)==2); break;
+  case 3: assert(va_arg(vl, double)==3.0); break;
+  }
+
+  va_end(vl);
+}
diff --git a/regression/cbmc/va_list3/test.desc b/regression/cbmc/va_list3/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring