analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
Part of #1477. The `Stdlib` version is more readable and less error-prone because the `prefix`/`suffix` is a labeled argument, so there's no ambiguity which way the two string arguments are...
In SV-COMP no-overflow tasks there are cases similar to the following example: ```c int main() { int i = __VERIFIER_nondet_int(); int j = __VERIFIER_nondet_int(); if (!(i==0 && j==0)) return 0;...
In SV-COMP no-overflow tasks there are cases similar to the following example: ```c int counter = 0; int main() { int X = __VERIFIER_nondet_int(); long long x = 0; while...
For #1508 I was playing around with various configurations to check that they still work, and it seems that Goblint allows to have an analysis that is path-sensitive, but not...
The following issue popped up when doing intensive sv-comp tests: ```c //SKIP PARAM: --enable ana.int.interval --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none int a; int main() { a = 5; a...
Lookahead widening from https://link.springer.com/chapter/10.1007/11817963_41 ### TODO - [x] Add option. - [x] Implement `threadenter`. - [x] Add @sim642's tests: https://github.com/goblint/analyzer/compare/master...ronald. - [x] Merge `master`. - [ ] Decide what to...
This is on top of #1500. It is a continuation of #1430. The fix from #1500 made it possible to replace the remaining usages of addresses with mvals with definite...
Straight from `no-overflow` on `ldv-regression/test_overflow.i` ; we are not flagging any overflow here. ```c #include #include void __blast_assert() { ERROR: {reach_error();abort();} } ssize_t getService(); int globalSize; int main(int argc, char*...
The following popped up when doing extensive benchmarking, so by creduce we get: ```c //SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain octagon --set sem.int.signed_overflow assume_none #include #include long *a; pthread_t...
The destabilize_vs function is an almost verbatim copy of destabilize_normal, except that it is supposed to determine whether any called or start variables were destabilized. This is needed for the...
