Add float tests

Author: peterschrammel

regression/cbmc-shadow-memory/float1/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  // field declarations
+  __CPROVER_field_decl_local("field1", (unsigned __CPROVER_bitvector[7])0);
+
+  unsigned __CPROVER_bitvector[7] v;
+  float x;
+  assert(!__CPROVER_get_field(&x, "field1"));
+
+  __CPROVER_set_field(&x, "field1", v);
+  assert(__CPROVER_get_field(&x, "field1") == v);
+
+  return 0;
+}

regression/cbmc-shadow-memory/float1/test.desc

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