Simmo Saan
Simmo Saan
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...
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...
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...
### 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...
`UpdateCil` updates IDs of statements (`sid`) and variables (`vid`), but not `compinfo` keys (`ckey`). I already wondered this in #598 but now here's concrete evidence that not updating them causes...