analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
This is an attempt to address https://github.com/goblint/analyzer/issues/101#issuecomment-1200996946 and https://github.com/goblint/analyzer/pull/809#discussion_r935693299 by adding more lval lattice tests for _some_ possibly reasonable structure and getting them to pass. I've opened this separate from...
Version 2.0.0 release on opam reveals the following float domain test failures on arm64: - [ ] :1:floatDomainTest:3:float_interval_qcheck64:4:test_FI_lt_xor_ge - [ ] :1:floatDomainTest:3:float_interval_qcheck64:5:test_FI_gt_xor_le - [ ] :1:floatDomainTest:3:float_interval_qcheck64:6:test_FI_eq_xor_ne - [x] :1:floatDomainTest:0:float_interval32:5:test_FI_casti2f_specific -...
Version 2.0.0 release on opam reveals the following thread analysis crashes on alpine, which notably uses musl instead of glibc: - [ ] 10/25 tid-array-malloc - [ ] 10/26 tid-array-malloc-free...
Part of issue #545. This is a quick idea I had to move all the incrementally changed functions stuff out of TD3. The point is to expose separate constraint system...
Pulled out from #28 since most of the TODOs there are now done. This would gives us an additional safety guarantee that no options are modified after the solver has...
This was revealed by #345. Simply `get`-ing/`eval`-ing global constraint variables added bottom to `rho`. This unnecessarily increases rho with default values. This PR changes TD3 such that it doesn't store...
In the following example an integer is written through a char pointer. The following assert should fail, because only part of the integer value was overwritten. But currently the assert...
### Links In my attempt to understand the Hoare powerset domain (`SetDomain.Hoare`) used for path-sensitivity I happened upon the following: * [some slides from Miné](https://www.di.ens.fr/~rival/semverif-2017/sem-13-ai.pdf) (slide 20), * and referred...
In #278 all the `assert`s in tests were changed to `__goblint_check`, which is declared by a `goblint.h` header that we forcefully include into every analyzed file via `-include`. This makes...