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

Robust ctags #117

Closed markrtuttle closed 2 years ago

markrtuttle commented 2 years ago

This pull request implements robust support for ctags. This resolves https://github.com/model-checking/cbmc-viewer/issues/101.

Viewer adds to the symbol definitions found in the goto binary symbol table whatever symbol definitions ctags can find in the source files mentioned in the symbol table. This adds, for example, definitions of type symbols.

There are three generations of ctags. Universal ctags replaced exhuberant ctags replaced legacy ctags. This code change invokes ctags using the universal API and then the exhuberant API and then the legacy API. It uses the symbols returned by the first successful invocation, and continues without ctags symbols if no invocation is successful (for example, if ctags is not even installed).

This was tested on the HTTP proofs by running master with universal ctags and using this branch with universal, exhuberant, and legacy ctags. Then the files viewer-symbol.json for each proof were compared. Using universal and exhuberant ctags with master and this branch, the results were identical. Using legacy with master and this branch, the master invocation failed, but this branch returned symbols that were a strict subset of the symbols returned with universal and exhuberant. (That is not quite true: legacy picked up a dozen names of formal parameters used in function prototypes in header file that universal and exhuberant correctly ignored.)

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