Reporting Verification Results

Any verification errors reported by Dafny indicate the line and column number at which they occur. These correspond to the emitted Dafny code. To meaningfully display these back to a user, they are translated to positions in the original Python source. This is done using a reverse-lookup of a mapping stored between Python and Dafny code as the latter is emitted.

The following is an example Dafny error message:

program.dfy(1,16): Error: A postcondition might not hold on this return path.

The line and column number is extracted from the message. This is used to find the nearest Dafny segment stored in the mapping created during the printing of the code from its AST. A pair of segments p1 are nearer than another pair p2 if either of the following conditions hold:

1. the absolute difference in line numbers of p1 is less than that of p2
2. the absolute difference in line numbers of p1 is equal to that of p2 and the absolute difference in column numbers of p1 is less than than that of p2

Having obtained the nearest Dafny segment, its corresponding Python segment is obtained from the mapping and its information presented to the user:

Line: 2 Column: 4 Value: ==, Error, A postcondition might not hold on this return path.

The error message is left unchanged from that given by Dafny. This is fine as the verification error messages do not refer to specific constructs in the program.