Skip to content

Commit 295a552

Browse files
authored
Merge pull request #804 from peterschrammel/bugfix/exit-code-on-error
Fix translation of safety checker status to exit codes
2 parents 1bb1aaa + b12e408 commit 295a552

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
@@ -1011,17 +1011,28 @@ int cbmc_parse_optionst::do_bmc(
10111011
{
10121012
bmc.set_ui(get_ui());
10131013

1014+
int result=6;
1015+
10141016
// do actual BMC
1015-
bool result=(bmc.run(goto_functions)==safety_checkert::SAFE);
1017+
switch(bmc.run(goto_functions))
1018+
{
1019+
case safety_checkert::SAFE:
1020+
result=0;
1021+
break;
1022+
case safety_checkert::UNSAFE:
1023+
result=10;
1024+
break;
1025+
case safety_checkert::ERROR:
1026+
result=6;
1027+
break;
1028+
}
10161029

10171030
// let's log some more statistics
10181031
debug() << "Memory consumption:" << messaget::endl;
10191032
memory_info(debug());
10201033
debug() << eom;
10211034

1022-
// We return '0' if the property holds,
1023-
// and '10' if it is violated.
1024-
return result?0:10;
1035+
return result;
10251036
}
10261037

10271038
/*******************************************************************\

0 commit comments

Comments
 (0)