Skip to content

Commit 2df2abb

Browse files
author
martin
committed
Change a few erronious return codes so that they are more internally consistent.
1 parent cf96cef commit 2df2abb

File tree

1 file changed

+6
-5
lines changed

1 file changed

+6
-5
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

+6-5
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,7 @@ int goto_instrument_parse_optionst::doit()
125125
if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
126126
{
127127
help();
128-
return CPROVER_EXIT_SUCCESS;
128+
return CPROVER_EXIT_USAGE_ERROR;
129129
}
130130

131131
eval_verbosity();
@@ -716,7 +716,7 @@ int goto_instrument_parse_optionst::doit()
716716
{
717717
error() << "Failed to open output file "
718718
<< cmdline.args[1] << eom;
719-
return CPROVER_EXIT_USAGE_ERROR;
719+
return CPROVER_EXIT_CONVERSION_FAILED;
720720
}
721721

722722
horn_encoding(goto_model, out);
@@ -748,13 +748,13 @@ int goto_instrument_parse_optionst::doit()
748748

749749
if(write_goto_binary(
750750
cmdline.args[1], goto_model, get_message_handler()))
751-
return CPROVER_EXIT_USAGE_ERROR;
751+
return CPROVER_EXIT_CONVERSION_FAILED;
752752
else
753753
return CPROVER_EXIT_SUCCESS;
754754
}
755755

756756
help();
757-
return CPROVER_EXIT_SUCCESS;
757+
return CPROVER_EXIT_USAGE_ERROR;
758758
}
759759

760760
catch(const char *e)
@@ -769,8 +769,9 @@ int goto_instrument_parse_optionst::doit()
769769
return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
770770
}
771771

772-
catch(int)
772+
catch(int e)
773773
{
774+
error() << "Numeric exception : " << e << eom;
774775
return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT;
775776
}
776777

0 commit comments

Comments
 (0)