Merge pull request #5669 from tautschnig/decl-side-effect

Cleanup side effects in declaration initialisers

Author: kroening

regression/cbmc/Sideeffects7/main.c

@@ -0,0 +1,20 @@
+int foo()
+{
+  __CPROVER_assert(0, "");
+}
+
+int main()
+{
+  struct
+  {
+    int a : 2;
+  } b;
+  int c;
+  short d;
+  // this is to make sure the fix for the below assignment does not introduce a
+  // new bug
+  d |= b.a = c >= 0;
+
+  // we previously weren't able to handle the below
+  short a = (a ^= 0) || foo();
+}

regression/cbmc/Sideeffects7/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+Invariant check failed
+--
+This example previously failed with an unhandled side effect in symex.

src/goto-programs/goto_convert.cpp

@@ -633,10 +633,15 @@ void goto_convertt::convert_decl(
     // Decl must be visible before initializer.
     copy(tmp, DECL, dest);
 
-    code_assignt assign(code.op0(), initializer);
-    assign.add_source_location()=tmp.source_location();
+    clean_expr(initializer, dest, mode);
 
-    convert_assign(assign, dest, mode);
+    if(initializer.is_not_nil())
+    {
+      code_assignt assign(code.op0(), initializer);
+      assign.add_source_location() = tmp.source_location();
+
+      convert_assign(assign, dest, mode);
+    }
   }
 
   // now create a 'dead' instruction -- will be added after the

src/goto-programs/goto_convert_side_effect.cpp

@@ -128,8 +128,24 @@ void goto_convertt::remove_assignment(
   // revert assignment in the expression to its LHS
   if(result_is_used)
   {
-    exprt lhs;
-    lhs.swap(to_binary_expr(expr).op0());
+    exprt lhs = to_binary_expr(expr).op0();
+    // assign_* statements can have an lhs operand with a different type than
+    // that of the overall expression, because of integer promotion (which may
+    // have introduced casts to the lhs).
+    if(expr.type() != lhs.type())
+    {
+      // Skip over those type casts, but also
+      // make sure the resulting expression has the same type as before.
+      DATA_INVARIANT(
+        lhs.id() == ID_typecast,
+        id2string(expr.id()) +
+          " expression with different operand type expected to have a "
+          "typecast");
+      DATA_INVARIANT(
+        to_typecast_expr(lhs).op().type() == expr.type(),
+        id2string(expr.id()) + " type mismatch in lhs operand");
+      lhs = to_typecast_expr(lhs).op();
+    }
     expr.swap(lhs);
   }
   else