goblint / analyzer / 4227

push

github

Warn when ana.opt.hashcons is disabled but implicitly overridden, fail for Apron (#1921)

* Initial plan

* Add warning when hashconsing is force-enabled

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Add test for hashcons warning

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Fix missing semicolon in warning logic

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Final: Complete implementation with warnings

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Move hashcons warning to check_arguments in maingoblint.ml

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Remove tests as they are not needed

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Remove _codeql_detected_source_root file

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Change Apron hashcons check to fail and use usesApron flag

- Add usesApron flag to MCPRegistry.spec_modules
- Add optional ~usesApron parameter to register_analysis (default false)
- Add any_activated_uses_apron() function to check registry
- Mark Apron analyses with ~usesApron:true flag
- Change warning to fail when hashcons disabled with Apron

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Swap order of Apron and ARG hashcons checks

Check Apron first (fail) before ARG (warn) since fail is more severe

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

6 of 10 new or added lines in 3 files covered. (60.0%)

22715 of 34662 relevant lines covered (65.53%)

403171.67 hits per line