Add regression tests for --nondet-volatile-model

Author: danpoe

regression/goto-instrument/nondet-volatile-model-01/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+volatile int a;
+volatile int b;
+
+int model()
+{
+  int value;
+  __CPROVER_assume(value >= 0);
+  return value;
+}
+
+void main()
+{
+  assert(a == 0);
+
+  assert(b >= 0);
+  assert(b == 0);
+  assert(b != 0);
+}

regression/goto-instrument/nondet-volatile-model-01/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--nondet-volatile-model b:model
+\[main.assertion.1\] line \d+ assertion a == 0: SUCCESS
+\[main.assertion.2\] line \d+ assertion b >= 0: SUCCESS
+\[main.assertion.3\] line \d+ assertion b == 0: FAILURE
+\[main.assertion.4\] line \d+ assertion b != 0: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that the read from b is modelled via the given model

regression/goto-instrument/nondet-volatile-model-02/test.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+volatile int a;
+volatile int b;
+volatile int c;
+
+int model()
+{
+  int value;
+  __CPROVER_assume(value >= 0);
+  return value;
+}
+
+void main()
+{
+  assert(a == 0);
+
+  assert(b >= 0);
+  assert(b == 0);
+  assert(b != 0);
+
+  assert(c >= 0);
+  assert(c == 0);
+  assert(c != 0);
+}

regression/goto-instrument/nondet-volatile-model-02/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--nondet-volatile-variable b --nondet-volatile-model c:model
+\[main.assertion.1\] line \d+ assertion a == 0: SUCCESS
+\[main.assertion.2\] line \d+ assertion b >= 0: FAILURE
+\[main.assertion.3\] line \d+ assertion b == 0: FAILURE
+\[main.assertion.4\] line \d+ assertion b != 0: FAILURE
+\[main.assertion.5\] line \d+ assertion c >= 0: SUCCESS
+\[main.assertion.6\] line \d+ assertion c == 0: FAILURE
+\[main.assertion.7\] line \d+ assertion c != 0: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that both options for selectively havocking/modelling volatile reads can
+be used together

regression/goto-instrument/nondet-volatile-model-03/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+volatile int a;
+volatile int b;
+
+int model_a()
+{
+  return 1;
+}
+
+int model_b()
+{
+  return 2;
+}
+
+void main()
+{
+  int result = a + b;
+  assert(result == 3);
+}

regression/goto-instrument/nondet-volatile-model-03/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--nondet-volatile-model a:model_a --nondet-volatile-model b:model_b
+\[main.assertion.1\] line \d+ assertion result == 3: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+--
+Checks that two volatile reads in the same expression can both be modelled by
+given functions