Skip to content

Commit b12e408

Browse files
Fix translation of safety checker status to error codes
The bmc_cover returns true on error which is translated into safety_checkert::ERROR in bmc.cpp, which was then incorrectly translated into exit code 10 instead of 6. Fixes diffblue/test-gen#201.
1 parent ae0ab67 commit b12e408

File tree

1 file changed

+15
-4
lines changed

1 file changed

+15
-4
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1045,17 +1045,28 @@ int cbmc_parse_optionst::do_bmc(
10451045
{
10461046
bmc.set_ui(get_ui());
10471047

1048+
int result=6;
1049+
10481050
// do actual BMC
1049-
bool result=(bmc.run(goto_functions)==safety_checkert::SAFE);
1051+
switch(bmc.run(goto_functions))
1052+
{
1053+
case safety_checkert::SAFE:
1054+
result=0;
1055+
break;
1056+
case safety_checkert::UNSAFE:
1057+
result=10;
1058+
break;
1059+
case safety_checkert::ERROR:
1060+
result=6;
1061+
break;
1062+
}
10501063

10511064
// let's log some more statistics
10521065
debug() << "Memory consumption:" << messaget::endl;
10531066
memory_info(debug());
10541067
debug() << eom;
10551068

1056-
// We return '0' if the property holds,
1057-
// and '10' if it is violated.
1058-
return result?0:10;
1069+
return result;
10591070
}
10601071

10611072
/*******************************************************************\

0 commit comments

Comments
 (0)