Set exit code to non-zero when verification fails

[atomb]

Currently, the only way to determine that verification has failed when running Boogie from the command line is the presence of error messages in the textual output. It should also return a non-zero exit code in that situation.

[atomb]

The logic appears to be in place to do this, but doesn't seem to work. For example:

boogie -trace Test/test21/Maps0.bpl
Parsing Test/test21/Maps0.bpl
Coalescing blocks...
Inlining...

Running abstract interpretation...
  [0.049955 s]

Verifying P ...
[TRACE] Using prover: z3
  [0.128 s, solver resource count: 6623, 5 proof obligations]  error
Test/test21/Maps0.bpl(27,3): Error: this assertion could not be proved
Execution trace:
    Test/test21/Maps0.bpl(18,3): anon0

Verifying Q ...
  [0.012 s, solver resource count: 5290, 1 proof obligation]  error
Test/test21/Maps0.bpl(36,3): Error: this assertion could not be proved
Execution trace:
    Test/test21/Maps0.bpl(36,3): anon0

Verifying R ...
  [0.012 s, solver resource count: 8603, 5 proof obligations]  error
Test/test21/Maps0.bpl(57,3): Error: this assertion could not be proved
Execution trace:
    Test/test21/Maps0.bpl(45,9): anon0

Boogie program verifier finished with 0 verified, 3 errors
$ echo $?
0

[shazqadeer]

It looks like Boogie expects to return exit code 1 only if the prover dies or the input programmer uses a feature unsupported by monomorphization without using /monomorphize flag. So, there appears to be an explicit decision to return exit code 0 for typing errors, verification failure errors, etc.

I don't know what the standard expectation for exit codes is.

[bkragl]

There was some (eventually abandoned) discussion on this exact topic a couple of years back in #13. Seems like there was general agreement with some unresolved details.