Skip annotation of the "source files" in the CBMC implementation.

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

Skip annotation of the "source files" in the CBMC implementation. #4

Closed markrtuttle closed 4 years ago

markrtuttle commented 4 years ago

The goto symbol table sometimes refers to files that are part of the CBMC implementation (eg, gcc_builtin_headers_types.h) and not available for source code annotation. This patch adds exception handling (try/except) to deal with missing "source files" listed in the symbol table.

Issue #, if available:

Description of changes:

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