Goto crossing scopes: fix scope tree entry of conditions

We must convert the condition of an if/then/else first to make sure any
declarations produced by converting the condition have a suitable
scope-tree node. Previously, gotos in either branch of the if-then-else
were led to believe that declarations resulting from condition were not
yet in scope. The feature from diffblue#8091 would, thus, result in a spurious
loop back to the declaration to put it in scope before following the
goto edge.

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/goto-programs/goto_convert.cpp

@@ -1611,6 +1611,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);
@@ -1620,9 +1623,6 @@ void goto_convertt::convert_ifthenelse(
   if(has_else)
     convert(code.else_case(), tmp_else, mode);
 
-  exprt tmp_guard=code.cond();
-  clean_expr(tmp_guard, dest, mode);
-
   generate_ifthenelse(
     tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
 }