tests from Dan

regression/ansi-c/sizeof4/main.c

@@ -0,0 +1,12 @@
+
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1];
+
+// The result of boolean operators is always an int
+STATIC_ASSERT(sizeof(1.0 && 1.0)==sizeof(int));
+STATIC_ASSERT(sizeof(1.0 || 1.0)==sizeof(int));
+STATIC_ASSERT(sizeof(!1.0)==sizeof(int));
+
+int main()
+{
+}

regression/ansi-c/sizeof4/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/enum6/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main(void)
+{
+  enum A { zero, one, two, three } a = two, b = one, c = three;
+
+  a <<= b;
+  assert(a==4);
+
+  c += b;
+  assert(c==4);
+
+  enum E { fortytwo=42 } e = fortytwo;
+  double res;
+  res = -42.0 + (double) e;
+  assert ((res >= -0.000005) && (res <= 0.000005));
+
+  return 0;
+}

regression/cbmc/enum6/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring