More constant propagation

Constant propagation now yields different right-hand sides in a test.

Author: tautschnig

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -3,7 +3,7 @@ Test.class
 --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

regression/cbmc/constant_folding3/main.c

@@ -0,0 +1,18 @@
+typedef struct _pair
+{
+  int x;
+  int y;
+} pair;
+
+int __VERIFIER_nondet_int();
+
+int main(void)
+{
+  pair p1 = {.x = 0, .y = __VERIFIER_nondet_int()};
+  pair p2 = {};
+  p2.x = __VERIFIER_nondet_int();
+
+  __CPROVER_assert(p1.x == p2.y, "true by constant propagation");
+
+  return 0;
+}

regression/cbmc/constant_folding3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Generated 1 VCC\(s\), 0 remaining after simplification$
+--
+^warning: ignoring

src/goto-symex/goto_symex_state.cpp

@@ -155,6 +155,8 @@ class goto_symex_is_constantt : public is_constantt
       */
       return false;
     }
+    else if(expr.id() == ID_nondet_symbol)
+      return true;
 
     return is_constantt::is_constant(expr);
   }

src/util/expr_util.cpp

@@ -276,8 +276,12 @@ bool is_constantt::is_constant_address_of(const exprt &expr) const
 
     return is_constant(deref.pointer());
   }
-  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;
 }