CBMC incorrectly simplifies the goto program in the test_gen branch

[lucasccordeiro]

In Cristina's exception_handling (https://github.com/cristina-david/cbmc/tree/exception_handling) branch, CBMC incorrectly simplifies the following C++ program.

#include <assert.h>
bool nondet_bool();
int main() {
  bool a=0;
  try {
    if (a)
      throw 2;
    else
      assert(0);
  }
  catch(char e) {
    return 1; 
 }
  return 0;
}

If we call CBMC as follows:
$cbmc main.cpp --show-goto-functions

Then we get this (fragment of) goto program:

main() /* main */
// 0 file main.cpp line 4 function main
_Bool a;
// 1 file main.cpp line 4 function main
a = (_Bool)0;
// 2 file main.cpp line 5 function main
CATCH-PUSH char->2
// 3 file main.cpp line 7 function main
THROW signed_int: irep("("side_effect" "" ("constant" "type" ("signedbv" "width" ("32") "#c_type" ("signed_int")) "value" ("00000000000000000000000000000010") "#source_location" ("" "file" ("main.cpp") "line" ("7") "function" ("main") "working_directory" ("/home/lucascordeiro/exception_handling/regression/cbmc-cpp/try-catch_simple_21")) "#base" ("10")) "type" ("") "statement" ("throw") "exception_list" ("exception_list" "" ("signed_int")))")
// 4 file main.cpp line 7 function main
GOTO 1
// 5 file main.cpp line 9 function main
ASSERT (_Bool)0 // assertion 0
// 6 no location
1: CATCH-POP
// 7 no location
GOTO 3
// 8 file main.cpp line 11 function main
2: char e;
// 9 file main.cpp line 12 function main
main#return_value = 1;
// 10 file main.cpp line 12 function main
dead e;
// 11 file main.cpp line 12 function main
dead a;
// 12 file main.cpp line 12 function main
GOTO 4
// 13 file main.cpp line 14 function main
3: main#return_value = 0;
// 14 file main.cpp line 14 function main
dead a;
// 15 no location
4: END_FUNCTION

The code that leads to this wrong simplification is related to the following method (originally from the test_gen branch):

/*******************************************************************\

Function: goto_convertt::finish_guarded_gotos

Inputs: Destination goto program

Outputs:

Purpose: For each if(x) goto z; goto y; z: emitted,
see if any destructor statements were inserted
between goto z and z, and if not, simplify into
if(!x) goto y;

*******************************************************************/
void goto_convertt::finish_guarded_gotos(goto_programt &dest)
{
....
}

@peterschrammel and @smowton : As we have discussed at diffblue, can you please take a look at this issue?

[smowton]

Embarrassingly, this is me using the is-guarded-goto variable uninitialised. Fix: smowton@7b4d670

[cristina-david]

@mgu: can you please review this?

[mgudemann]

LGTM
the change initializes the Boolean value to false which is the expected value for the control flow in the program. In C++, variables do not have a default init value.

[mgudemann]

the original PR was not included into test_gen, the new PR is for cbmc-testgen

[peterschrammel]

obsolete