More constant propagation

This also fixes a previously expected-to-fail regression test. Constant
propagation now yields different right-hand sides in a test.

Author: tautschnig

regression/cbmc-java/dynamic-multi-dimensional-array/test.desc

@@ -1,10 +1,5 @@
 CORE
 TestClass.class
 --function TestClass.f --cover location --unwind 2
-Source GOTO statement: .*
-(^ exception: Can't convert byte_extraction|Nested exception printing not supported on Windows)
-^EXIT=6$
---
---
-The exception thrown in this test is the symptom of a bug; the purpose of this
-test is the validate the output of that exception
+^EXIT=0$
+^SIGNAL=0$

regression/jbmc-strings/long_string/test_abort.desc

@@ -3,7 +3,7 @@ Test.class
 --refine-strings --function Test.checkAbort --trace
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_object[0-9]*=\(assignment removed\)
+dynamic_object[0-9]*=.*\?.*
 --
 --
 This tests that the object does not appear in the trace, because concretizing

src/goto-symex/goto_symex_state.cpp

@@ -83,7 +83,7 @@ void goto_symex_statet::level1t::operator()(ssa_exprt &ssa_expr)
 /// "constants"
 bool goto_symex_statet::constant_propagation(const exprt &expr) const
 {
-  if(expr.is_constant())
+  if(expr.is_constant() || expr.id() == ID_nondet_symbol)
     return true;
 
   if(expr.id()==ID_address_of)
@@ -187,13 +187,16 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   }
   else if(expr.id()==ID_member)
   {
-    if(expr.operands().size()!=1)
-      throw "member expects one operand";
+    const member_exprt &member_expr = to_member_expr(expr);
 
-    return constant_propagation_reference(expr.op0());
+    return constant_propagation_reference(member_expr.struct_op());
   }
-  else if(expr.id()==ID_string_constant)
+  else if(
+    expr.id() == ID_string_constant || expr.id() == ID_array ||
+    expr.id() == ID_struct || expr.id() == ID_union)
+  {
     return true;
+  }
 
   return false;
 }