Karoliine Holter
Karoliine Holter
While using the abstract debugger on an analysis that used `svcomp24` configuration, adding a breakpoint to a program point that had a warning showed a greyed-out breakpoint with the message...
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...
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 (&...
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...
When running the following modifications of test `01-oob-heap-simple.c`: ```c // PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval #include int main(int argc, char const *argv[]) { char *ptr = malloc(5 * sizeof(char));...
When `merge_inlines` is `false`, extern inline functions that are used several times produce one CFG with as many duplicate paths as there are usages. Here is an example to reproduce:...
* [Removes dead code](https://github.com/goblint/analyzer/commit/9485208d7c9898a4c61c9139ea5fe351ca03e809) that indicates as if we are not writing to known addresses if a pointer contains an unknown element, solves #1461 * Fixes issue #1465, and replaces...
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...