Hi all,
I’ve been building adalang_analyzer, an independent command-line static analyzer for Ada built on Libadalang (not affiliated with or endorsed by AdaCore). It’s now at 1.0.0-rc1, with an Alire package submitted (alire-index#2049, currently under review).
It covers coding-policy checks (restricted constructs, safety/numerical rules), intraprocedural data/control-flow defects (dead stores, uninitialized reads, dead code, division-by-zero, etc.), SPARK-readiness checks, and an optional bounded scalar --verify mode.
Rather than trusting hand-written fixtures alone, I’ve been running it against real open-source Ada/SPARK corpora (Tokeneer, CubedOS, SPARKNaCl, Saatana, AWS, Ada_Drivers_Library, Simple Components) and publishing the raw results, both hits and misses:
- On the AdaCore/SPARK2014 Tokeneer port (120 files), the first pass found and fixed 4 real analyzer false-positive classes, cutting reported violations from 1230 to 653 on the same corpus.
- On
--verifyvs. GNATprove on fully-proved corpora (SPARKNaCl, Saatana), zero cases where the analyzer called something safe that GNATprove couldn’t prove, and zero false “definite error” calls, across ~1000 matched proof obligations. - Along the way it also turned up a genuine bug in someone else’s code — a copy-paste condition (
X > 0 and then X > 0instead of comparing two different operands) in Dmitry Kazakov’s Simple Components, reported upstream.
Since this targets safety-relevant Ada, I’d really value review from people with Ada/SPARK or static-analysis background — either running it against your own codebase and reporting precision issues, or reviewing the check implementations directly. Repo, full corpus write-ups, and positioning/scope docs are here: GitHub - mmartign/AdaLang_Analyzer: AdaLang Analyzer is a command-line static analysis tool for Ada source code that uses Libadalang to detect rule violations and report them with explanations and remediation guidance. · GitHub
Feedback, bug reports, and PRs all welcome (GPL-3.0-or-later).
Maurizio