Support SARIF output format

[ligurio]

The Static Analysis Results Interchange Format (SARIF) is an industry standard format for the output of static analysis tools. Github supports SARIF format and allows showing code annotations in a pull requests ¹.

cbmc-viewer already helps to analyze results produced by CBMC, and it would be nice to implement exporting report to SARIF format.

Footnotes

1. https://github.com/sett-and-hive/sarif-to-comment-action?tab=readme-ov-file#example-usage ↩

[karkhaz]

Thank you for this suggestion! As far as I can tell, we haven't looked into adding SARIF output either for CBMC or for Kani.

Currently we use a script that can run in a GitHub Action that summarizes the results of all the CBMC proofs in a repository. The script prints out the results in GitHub-compatible markdown; here's an example of a CI run summary that uses that code. However, it looks like SARIF has a much more native experience, here's a GitHub blog post that includes screenshots of how GitHub renders the SARIF information.

I'm going to put it on the agenda for our next team discussion. Might not have an update for this week, but we'll update the ticket as soon as we've discussed doing this. Thank you!

[ligurio]

BTW, there is an issue in CBMC repository diffblue/cbmc#6851 and PR diffblue/cbmc#8835 which adds support for option --sarif-ui.