Merge pull request diffblue#2665 from tautschnig/gcc-conditional-stmt

Clean GCC conditional expressions in right-hand sides of declarations

Author: Daniel Kroening

regression/cbmc/gcc_conditional_expr1/main.c

@@ -1,5 +1,8 @@
+#include <assert.h>
+
 int g, k;
 
+// See https://gcc.gnu.org/onlinedocs/gcc/Conditionals.html
 int main()
 {
   int r1, r2;
@@ -14,4 +17,10 @@ int main()
   assert(r2==1);
   assert(g==2);
   assert(k==0);
+
+  int in_decl = g++ ?: 0;
+  assert(in_decl == 2);
+  assert(g == 3);
+
+  return 0;
 }

src/goto-programs/goto_convert.cpp

@@ -758,7 +758,8 @@ void goto_convertt::convert_assign(
     (rhs.get(ID_statement) == ID_assign ||
      rhs.get(ID_statement) == ID_postincrement ||
      rhs.get(ID_statement) == ID_preincrement ||
-     rhs.get(ID_statement) == ID_statement_expression))
+     rhs.get(ID_statement) == ID_statement_expression ||
+     rhs.get(ID_statement) == ID_gcc_conditional_expression))
   {
     // handle above side effects
     clean_expr(rhs, dest, mode);