analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
Ultimate revealed some incorrect witness invariants that we output: https://struebli.informatik.uni-freiburg.de/logs/concurrency-witnesses/20240205-105808-concurrency-witnesses-d8006e4be6-M/tabledef.table.html#/table?sort=1_Violation_4,asc&filter=1(4*Violation*(value(invariant))). - [x] `c/weaver/chl-collitem-subst.wvr.c`, line 107. We state invariant `b != 0` before `assume_abort_if_not(b = b - 2147483648);`, probably due to...
Frustrated with the syntactic loop unrolling (#563), this is a quick shot at a semantic one that I've wanted for a long time: just use path sensitivity to count and...
Our messages contain various redundant information which makes the messages long and harder to read. Based on some option we could try to produce simpler output for some things: -...
This is on top of #1216 as an attempt to make it handle disjunctive relational invariants. It "works" except there are some very odd fixpoint errors that I'll have to...
In 7edfff066099e9b96ceee39ea3250a62707727b1 of #1326 an `Obj`-related bug was found which wasn't caught by the OCaml typechecker due to the `Obj`. Although there's no simple way to avoid the use of...
Originally considered in https://github.com/goblint/analyzer/pull/1312#discussion_r1447107627. The problem is that `create_var` identifies variables purely by their name to compute an incremental-friendly `vid`. This could be fixed by replacing all use of `create_var`...
Depends on https://github.com/goblint/cil/pull/161. --- The tests with annotations will come in very few days. We are sorry for this (right now still) unpolished state. Changes in goblint-cil: - asm is...
We have quite often suspected excessive widening at unknowns that receive side-effects (e.g. function entry nodes) as a cause of unnecessary precision-loss. In a brainstorming session with @stilscher and @hseidl...
Looking into the warnings of context-sensitive analyses of the Concrat benchmarks revealed that for the `Signed integer overflow and underflow`, there are, in some cases, duplicate warnings for the same...
As discussed in https://github.com/goblint/analyzer/pull/1193#issuecomment-1735806541 and the following comments, it might be good to remove the duplicate access handling done in the useAfterFree analysis and reuse the events already produced by...