From 96d345b55c38c9590d58027f67ca4b67fbeb56b1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 2 Aug 2018 15:49:53 +0000 Subject: [PATCH] Clean GCC conditional expressions in right-hand sides of declarations Fixes: #2662 --- regression/cbmc/gcc_conditional_expr1/main.c | 9 +++++++++ src/goto-programs/goto_convert.cpp | 3 ++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/gcc_conditional_expr1/main.c b/regression/cbmc/gcc_conditional_expr1/main.c index 5f6f46bbba4..baa0cf0659a 100644 --- a/regression/cbmc/gcc_conditional_expr1/main.c +++ b/regression/cbmc/gcc_conditional_expr1/main.c @@ -1,5 +1,8 @@ +#include + 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; } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 2e495fa4d59..7b82b3415c3 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/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);