test for printf

Author: Daniel Kroening

regression/cbmc/printf1/main.c

@@ -0,0 +1,11 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main()
+{
+  printf("PRINT d1 %d, %d\n", 123, -123);
+  printf("PRINT g1 %g, %g, %g, %g\n", 123.0, -123.0, 123.123, 0.123);
+  printf("PRINT e1 %e, %e, %e, %e\n", 123.0, -123.0, 123.123, 0.123);
+  printf("PRINT f1 %f, %f, %f, %f\n", 123.0, -123.0, 123.123, 0.123);
+  assert(0);
+}

regression/cbmc/printf1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^PRINT d1 123, -123$
+^PRINT g1 123, -123, 123\.123, 0\.123$
+^PRINT e1 1\.230000e\+2, -1\.230000e\+2, 1\.231230e\+2, 1\.230000e-1$
+^PRINT f1 123\.000000, -123\.000000, 123\.123000, 0\.123000$
+--
+^warning: ignoring