analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
This fixes an assert failing in `sv-benchmarks/c/recursive/MultCommutative-2` here: https://github.com/goblint/analyzer/blob/a4e917f86c983d7c97138364b07e031a7715e3d5/src/analyses/base.ml#L2216-L2220 The problem was that `ID.is_bool value = true` but `ID.to_bool = None`, which of course shouldn't happen. The offending `value` is...
Adds an option that tries choosing some configurations automatically based on the file that is analyzed. Already implemented: - Enable Congruence domain only in functions that use modulo and related...
Related to issues #101 and #803. ### TODO - [x] Benchmark on sv-benchmarks. - [x] Check performance on SQLite. - [x] Fix termination issue when `SetDomain.Joined` is used inside `AddressDomain`?...
This PR adds an unassume analysis, which loads a YAML witness before solving and emits `Unassume` events during the analysis at nodes which have invariants. Both base, apron and var_eq...
In #210 it came up multiple times that OCaml's standard [`Format`](https://ocaml.org/api/Format.html) module could replace [`Pretty`](https://people.eecs.berkeley.edu/~necula/cil/api/Pretty.html) from CIL with additional benefits: 1. It's maintained in OCaml's standard library while `Pretty` isn't...
As discussed in GobCon, this would be something to somewhat limit the large number of invariants we generate. Since accesses are to lvalues, not just variables, this also has lvalue...
Here's a wild idea I toyed with, which we can either make complete or just close this PR. Basically, dune's Cram tests are designed for testing executables and could have...
This ~~hopefully~~ fixes _all_ remaining `ERROR (verify)` results on sv-benchmarks ([Full table](https://goblint.cs.ut.ee/results/85-all-fast-hoaredomain-after-bool-range/table-generator.table.html#/table)). It is on top of #809 since that causes significant changes to `ERROR (verify)` results. ### Changes 1....
The use of `AD.meet` to check address set must-not-equality: https://github.com/goblint/analyzer/blob/3a189a9e85e9f494f40e44012f864e663274181b/src/analyses/base.ml#L331-L334 is unsound in at least the following cases: - [ ] First struct field and zero index: https://github.com/goblint/analyzer/blob/3a189a9e85e9f494f40e44012f864e663274181b/tests/regression/02-base/91-ad-meet.c#L6-L16 - [...
Every now and then we've had unsoundness issues at branches which have both (true and false) outgoing edges `raise Deadcode` and yield bottom states. We should have a sanity check...