kind2-mc/kind2

Exit code 20 on a seemingly successful analysis

Closed this issue · 2 comments

erooke commented

When running kind on the command line successful checks seem to return an exit code of 20 despite nothing going wrong. Given the following file as input:

node Id(x: bool) returns (y: bool) ;
(*@contract import
  IdCon(x) returns (y) ;
*)
let
  --%MAIN;
  y = x;
tel

contract IdCon(x: bool) returns (y: bool);
let
  guarantee x = y ;
tel

Running kind2 produces the following output

$ kind2 trivial.lus
 kind2 v1.6.0-86-g4417dc5



=========================================================================================================================================
Analyzing Id
  with First top: 'Id' (no subsystems)

<Success> Property IdCon[l2c13].guarantee[l12c3] is valid by one state invariant generator (bool) after 0.042s.

-----------------------------------------------------------------------------------------------------------------------------------------
Summary of properties:
-----------------------------------------------------------------------------------------------------------------------------------------
IdCon[l2c13].guarantee[l12c3]: valid (at 1)
=========================================================================================================================================

$ echo "$?"
20

Is there something silently failing which I am missing which is triggering a non-zero exit code here?

System details:

  • kind2: v1.6.0-86-g4417dc5
  • Z3: version 4.11.2 - 64 bit
  • OS: Linux 6.0.2-arch1-1 x86_64
daniel-larraz commented

No, nothing is silently failing.

For historical reasons, Kind 2 does not follow the UNIX convention. It uses the following convention for exit codes:
0 = Unknown
2 = Error
10 = Unsafe
20 = Safe

Clearly we should document this atypical behavior.

daniel-larraz commented

We decided to change the behavior of Kind 2, and make Kind 2 follow the POSIX convention of returning exit code 0 for successful checks. PR #971 implements this change.

  • 🎉1