Add regression test of __CPROVER_DYNAMIC_OBJECT

Author: thomasspriggs

regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+void main()
+{
+  char local;
+  void *pointer = &local;
+  const bool make_dynamic = nondet_bool();
+  if(make_dynamic)
+  {
+    pointer = malloc(1);
+  }
+  assert(__CPROVER_DYNAMIC_OBJECT(pointer));
+}

regression/cbmc-incr-smt2/dynamic-memory/assert_dynamic.desc

@@ -0,0 +1,11 @@
+CORE
+assert_dynamic.c
+--trace
+Passing problem to incremental SMT2 solving
+line 16 assertion __CPROVER_DYNAMIC_OBJECT\(pointer\)\: FAILURE
+make_dynamic\=FALSE
+^EXIT=10$
+^SIGNAL=0$
+--
+make_dynamic\=TRUE
+--

regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+void main()
+{
+  char local;
+  void *pointer = &local;
+  const bool make_dynamic = nondet_bool();
+  if(make_dynamic)
+  {
+    pointer = malloc(1);
+  }
+  assert(!__CPROVER_DYNAMIC_OBJECT(pointer));
+}

regression/cbmc-incr-smt2/dynamic-memory/assert_not_dynamic.desc

@@ -0,0 +1,11 @@
+CORE
+assert_not_dynamic.c
+--trace
+Passing problem to incremental SMT2 solving
+line 16 assertion \!__CPROVER_DYNAMIC_OBJECT\(pointer\)\: FAILURE
+make_dynamic\=TRUE
+^EXIT=10$
+^SIGNAL=0$
+--
+make_dynamic\=FALSE
+--

regression/cbmc-incr-smt2/dynamic-memory/valid.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+bool nondet_bool();
+
+void main()
+{
+  char local;
+  void *pointer = &local;
+  const bool make_dynamic = nondet_bool();
+  if(make_dynamic)
+  {
+    pointer = malloc(1);
+  }
+  assert(make_dynamic || !__CPROVER_DYNAMIC_OBJECT(pointer));
+}

regression/cbmc-incr-smt2/dynamic-memory/valid.desc

@@ -0,0 +1,10 @@
+CORE
+valid.c
+--trace
+Passing problem to incremental SMT2 solving
+line 16 assertion make_dynamic \|\| \!__CPROVER_DYNAMIC_OBJECT\(pointer\)\: SUCCESS
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+--