Simmo Saan
Simmo Saan
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`...
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...
Apron supports floating-point variables in addition to integer ones, so we could "just" use them. For example, Mopsa seems to as well. This requires some refactoring of the relational interfaces...
[Precise and modular static analysis by abstract interpretation for the automatic proof of program soundness and contracts inference](https://theses.hal.science/tel-02947214/) provides a more efficient join operator for Apron abstractions with heterogeneous environments...
Currently the abstract debugger uses the same ARG and CFG-location mappings as witnesses, including the same notion of synthetic locations. However, this is not ideal for abstract debugging, where too...