Merge pull request #5374 from danpoe/feature/selective-modelling-of-volatile-variables

Selective modelling of volatile variables

Author: danpoe

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

@@ -2,7 +2,7 @@ CORE
 test.c
 --nondet-volatile-variable x
 ^Invalid User Input$
-given name x does not represent a volatile variable with static lifetime$
+symbol `x` does not represent a volatile variable with static lifetime$
 ^EXIT=1$
 ^SIGNAL=0$
 --

regression/goto-instrument/nondet-volatile-04/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+volatile int x;
+int y;
+
+void main()
+{
+  y = x;
+  assert(x == y);
+}

regression/goto-instrument/nondet-volatile-04/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.c
+--nondet-volatile
+^\[main.assertion.1\] line \d+ assertion x == y: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check interaction between a volatile and a non-volatile variable

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

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

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+volatile int a;
+
+float model()
+{
+  return 1;
+}
+
+void main()
+{
+  a;
+}