analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
This PR improves the abstraction of the `cos` function if the argument is neither nan nor inf by - storing also the inverted relationship between arguments of math functions and...
It seems like Cirrus CI (which has unlimited free minutes for OpenSource projects) might have support here. Might make sense to set this up for the MacOS builds, even if...
For regression tests `28 78` and `28 79` there are warnings: ``` [Warning][Unknown] lval (& s)->datum points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:129-22:139) [Warning][Unknown] lval (&...
This PR implements a relational domain tracking substring relations between string variables. It adapts [Arceri et al.'s generic proposition](https://link.springer.com/chapter/10.1007/978-3-030-94583-1_2) to fit the special design of C-strings. The domain can be...
With the following loop implementation apron wasn't able to provide meaningful analysis for loop1, loop2 or res ``` int main() { int rows = 3; int columns = 4; int...
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...
[...] The invariant is given as `i#318-1/3j#319+1/3k#320+4/3=0` which then likely does not survive conversion to a CIL expression. I suggest we open a new issue, as this is a general...
By some miracle, I happened to analyze the `smtprc` from the bench repository with several `master` versions, revealing that a bug was introduced and then 'fixed' by merging an unrelated...
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...