search

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

Support SARIF output format #149

Open ligurio opened 2 months ago

ligurio commented 2 months ago

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 ^2.

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

[^1]: Github Documentation

karkhaz commented 2 months ago

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!