model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
https://model-checking.github.io/cbmc-viewer/
Apache License 2.0
32 stars 11 forks source link

Don't link error traces to library source files #47

Closed markrtuttle closed 3 years ago

markrtuttle commented 3 years ago

Issue #45, if available:

Issue https://github.com/awslabs/aws-viewer-for-cbmc/issues/45

Description of changes:

Viewer annotates only source files under SRCDIR, links steps of an error trace only to lines of code in files under SRCDIR, and uses path names relative to SRCDIR for files under SRCDIR. With RMC, we see for the first time errors triggered by lines of code in the RMC implementation (eg, the Rust standard library) not under SRCDIR, and viewer fails when it tries to generate a link to the line of code triggering the error (in a library source file given by an absolute path name).

With this commit, viewer will no longer try to link to a file specified with an absolute path name (to a file not under SRCDIR).

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.