Merge pull request #5360 from danpoe/fixes/nondet-volatile

Fix --nondet-volatile bug

Author: danpoe

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
+}

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

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);
 
@@ -88,7 +87,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())
     {

src/goto-instrument/nondet_volatile.h

@@ -14,10 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 #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