From fed55364d1bba8b97844dfa709b614f912236e07 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Wed, 27 May 2020 17:13:43 +0100
Subject: [PATCH 1/2] Fix --nondet-volatile bug where lhs was not considered in
 assignment

---
 regression/goto-instrument/nondet-volatile-01/test.c  | 11 +++++++++++
 .../goto-instrument/nondet-volatile-01/test.desc      |  9 +++++++++
 src/goto-instrument/nondet_volatile.cpp               |  2 +-
 3 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 regression/goto-instrument/nondet-volatile-01/test.c
 create mode 100644 regression/goto-instrument/nondet-volatile-01/test.desc

diff --git a/regression/goto-instrument/nondet-volatile-01/test.c b/regression/goto-instrument/nondet-volatile-01/test.c
new file mode 100644
index 00000000000..ec0cc273a79
--- /dev/null
+++ b/regression/goto-instrument/nondet-volatile-01/test.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void main()
+{
+  int a[2] = {0};
+
+  volatile int i = 0;
+  a[i] = 1;
+
+  assert(a[1] == 0); // should fail
+}
diff --git a/regression/goto-instrument/nondet-volatile-01/test.desc b/regression/goto-instrument/nondet-volatile-01/test.desc
new file mode 100644
index 00000000000..06b61f44592
--- /dev/null
+++ b/regression/goto-instrument/nondet-volatile-01/test.desc
@@ -0,0 +1,9 @@
+CORE
+test.c
+--nondet-volatile
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that volatile variables appearing in the lhs of an assignment are
+correctly treated as nondet
diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp
index 73a79937355..20d6517a22b 100644
--- a/src/goto-instrument/nondet_volatile.cpp
+++ b/src/goto-instrument/nondet_volatile.cpp
@@ -88,7 +88,7 @@ void nondet_volatile(
     if(instruction.is_assign())
     {
       nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs());
-      nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).rhs());
+      nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).lhs());
     }
     else if(instruction.is_function_call())
     {

From ff4a7b60aa407a89bdd943f75f166b4b004dc95a Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Wed, 27 May 2020 17:15:37 +0100
Subject: [PATCH 2/2] Remove obsolete declaration and make functions static for
 --nondet-volatile feature

---
 src/goto-instrument/nondet_volatile.cpp | 9 ++++-----
 src/goto-instrument/nondet_volatile.h   | 4 ----
 2 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp
index 20d6517a22b..96514c144e3 100644
--- a/src/goto-instrument/nondet_volatile.cpp
+++ b/src/goto-instrument/nondet_volatile.cpp
@@ -31,7 +31,7 @@ static bool is_volatile(const namespacet &ns, const typet &src)
   return false;
 }
 
-void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
 {
   Forall_operands(it, expr)
     nondet_volatile_rhs(symbol_table, *it);
@@ -52,7 +52,7 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
   }
 }
 
-void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
 {
   if(expr.id()==ID_if)
   {
@@ -75,9 +75,8 @@ void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
   }
 }
 
-void nondet_volatile(
-  symbol_tablet &symbol_table,
-  goto_programt &goto_program)
+static void
+nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
 {
   namespacet ns(symbol_table);
 
diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h
index dd92f3b1833..931478e96d1 100644
--- a/src/goto-instrument/nondet_volatile.h
+++ b/src/goto-instrument/nondet_volatile.h
@@ -14,10 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_model.h>
 
-bool is_volatile(
-  const symbol_tablet &,
-  const typet &);
-
 void nondet_volatile(goto_modelt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H