Merge pull request #8187 from tautschnig/bugfixes/no-spurious-loops

Goto crossing scopes: fix scope tree entry of conditions

Author: tautschnig

regression/cbmc/declaration-goto/no-duplicate-decl.c

@@ -0,0 +1,16 @@
+int foo()
+{
+  return 1;
+}
+
+int main()
+{
+  if(foo())
+    goto out;
+
+  return 1;
+
+out:
+  __CPROVER_assert(0, "false");
+  return 0;
+}

regression/cbmc/declaration-goto/no-duplicate-decl.desc

@@ -0,0 +1,11 @@
+CORE
+no-duplicate-decl.c
+--show-goto-functions
+^[[:space:]]*DECL main::\$tmp::return_value_foo
+^EXIT=0$
+^SIGNAL=0$
+--
+^[[:space:]]*DECL going_to::out
+^[[:space:]]*\d+: DECL main::\$tmp::return_value_foo
+--
+Test that no loop back to the declaration is generated.

regression/validate-trace-xml-schema/check.py

@@ -23,6 +23,7 @@
     ['xml-interface1', 'test_wrong_flag.desc'],
     # these want --show-goto-functions instead of producing a trace
     ['integer-assignments1', 'integer-typecheck.desc'],
+    ['declaration-goto', 'no-duplicate-decl.desc'],
     ['destructors', 'compound_literal.desc'],
     ['destructors', 'enter_lexical_block.desc'],
     ['enum_is_in_range', 'enum_test3-simplified.desc'],

src/ansi-c/goto-conversion/goto_convert.cpp

@@ -1597,6 +1597,9 @@ void goto_convertt::convert_ifthenelse(
     return convert_ifthenelse(new_if0, dest, mode);
   }
 
+  exprt tmp_guard = code.cond();
+  clean_expr(tmp_guard, dest, mode);
+
   // convert 'then'-branch
   goto_programt tmp_then;
   convert(code.then_case(), tmp_then, mode);
@@ -1616,9 +1619,6 @@ void goto_convertt::convert_ifthenelse(
                           : code.else_case().source_location();
   }
 
-  exprt tmp_guard = code.cond();
-  clean_expr(tmp_guard, dest, mode);
-
   generate_ifthenelse(
     tmp_guard,
     source_location,