- Improved Context Information for Verification Errors (#435). When a verification error occurred, it was often difficult to tell which part of a pre-condition / post-condition was causing it. Now, context information is included to identify the relevant part of the precondition or postcondition.
As an example to illustrate this context information, consider the following (incorrect) program:
function abs(int x) => (int r) ensures r == x || r == -x ensures r >= 0: // return x
Compiling this program using the previous version of the compiler (with verification enabled), produced the following error:
./test.whiley:5: postcondition not satisfied return x ^^^^^^^^
However, this does not tell us which component of the postcondition actually failed. Compiling with the new version gives the following error:
./test.whiley:5: postcondition not satisfied return x ^^^^^^^^ ./test.whiley:3: ensures r >= 0: ^^^^^^
Here, we see that the context information consists of additional point(s) in the program which are related. In this case, it tells us exactly which component of the postcondition is not satisfied.
As usual, you can get the latest files here: