Add Mopsa-like Warning Selectivity Reporting

[Robotechnic]

The PR adds a new kind of output inspired by this paper from R. Monat & al: https://inria.hal.science/hal-04652657v2. This output contains all the checks performed by the analyzer and their result of three types:

• Error: There will be an error in any possible cases
• Warning: There might be an error in some cases
• Safe: There can't be an error in any possible cases

This output only takes into account the following checks:

• Integer overflow/underflow
• Invalid array access
• Division by zero errors
• Assersion violations
• Unknown function ptr
• Double free
• Writing to string literals

[michael-schwarz]

There should be a reference added to Raphael Monat's paper proposing this approach.

[Robotechnic]

I think it's this one: https://inria.hal.science/hal-04652657v2

Should I add it to the code or just to the PR?

[michael-schwarz]

Yes! Please add it to the code as well!

[Copilot]

Pull request overview

This PR adds Mopsa-like warning selectivity reporting to Goblint, based on a research paper by Raphaël Monat et al. The feature tracks all checks performed during analysis and categorizes them as Error (will definitely fail), Warning (might fail), or Safe (cannot fail). This provides more detailed information about the analyzer's findings beyond traditional warning messages.

Key changes:

• Introduces a new Checks module to track and export check results
• Adds "dashboard" output format that includes files, timing, and check results as JSON
• Integrates check tracking throughout the codebase for integer overflow, array bounds, division by zero, assertions, memory access, double free, and string literal writes

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/common/util/checks.ml	New module implementing check tracking with Kind (Error/Warning/Safe) and Category enums, hash-based storage, and JSON export
src/util/timing/goblint_timing_intf.ml	Adds root_with_current function to get timing tree with in-progress resources
src/framework/analysisResultOutput.ml	Adds "dashboard" output format that exports files, timing, and checks as JSON
src/config/options.schema.json	Updates schema to include "dashboard" as a valid result format option
src/cdomain/value/cdomains/intDomain0.ml	Adds Checks.warn calls for integer overflow/underflow alongside existing warnings
src/cdomain/value/cdomains/int/intDomTuple.ml	Adds Checks.safe calls when overflow checks pass, with no_safe parameter to control reporting
src/cdomain/value/cdomains/arrayDomain.ml	Integrates check tracking for array bounds, negative array size, null byte checks, and buffer overflow detection
src/cdomain/value/cdomains/addressDomain.ml	Adds checks for writing to string literals
src/analyses/useAfterFree.ml	Adds check tracking for double free and use-after-free detection
src/analyses/memOutOfBounds.ml	Integrates check tracking throughout memory bounds analysis for various pointer and array access scenarios
src/analyses/baseInvariant.ml	Adds check tracking for division by zero in invariant analysis
src/analyses/base.ml	Integrates checks for division/modulo by zero, null pointer dereference, and invalid memory deallocation
src/analyses/assert.ml	Adds check tracking for assertion success, failure, and unknown outcomes

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.