Missing function/file/line information in trace

[carolynzech]

I tried Exercise 2 of the Bounds checking and pointers section of the tutorial. I ran

cargo kani --harness bound_check --visualize --enable-unstable

with Kani version: 0.53.0-dev

I expected to see information about the function, file, and line, e.g.:

Step XXX: Function bound_check, File src/bounds_check.rs, Line 37

Instead, I saw this:

Step XXX: Function MISSING, File MISSING, Line 0

for every line of the trace.

[tautschnig]

This appears to be a bug in what input we produce to CBMC Viewer as CBMC does report all the details correctly and Kani, in its default output, also knows about those source locations. In light of #3302 I am, however, wondering whether it is worth trying to fix this.

[carolynzech]

This appears to be a bug in what input we produce to CBMC Viewer as CBMC does report all the details correctly and Kani, in its default output, also knows about those source locations. In light of #3302 I am, however, wondering whether it is worth trying to fix this.

Probably not--if we're already deprecating it, doesn't seem worth it. Will close for now.