Manuel Pietsch

Autotuning of Configuration: First Steps

1

Adds an option that tries choosing some configurations automatically based on the file that is analyzed. Already implemented: - Enable Congruence domain only in functions that use modulo and related...

'make headers' does not create all required compiler-gcc headers

3

When running the regression tests with `./scripts/update_suite.rb` on my system, multiple tests complain that the file `linux-headers/include/linux/compiler-gcc12.h` is missing. This persists even after running `make header`. I am using zsh,...

Unsound no-overflow result in SV-COMP test with `bsearch`

1

For the sv-comp test `termination-crafted/Binary_Search-1.c` in the category no-overflow Goblint returns a wrong result. The problem is that it has a function bsearch, which also exists in includes/stdlib.c If I...

New Analysis combining Linear Two-Variable Equalities with other domains

3

This pull-request adds an analysis combining Lin2VarEq with multiple other domains: Intervals, Congruences and several options for two variable inequalities. Lin2VarEq selects a representant for each group of variables connected...

Termination analysis gives up for loops with multiple conditions

1

I came across the following (slightly adapted) program from sv-comp: ```c int main() { int c, x, y; c = 0; if (y > 46340) return 0; while ((x >...