SchiJoha

master thesis: Taming Recursion with Three Context-Sensitive Analyses (Callstring, LoopfreeCallstring, Context Gas)

3

Implementation of three context-sensitive approaches to tam recursion: - call string approach in the Sharir and Pnueli sense: a call stack tracking the last k function calls is used as...

If all analyses are context insensitive, the sv-comp testcase `goblint-regression/06-symbeq_04-funloop_hard1.i` fails with the `svcomp24.json` configuration. It seems that some analyses produce unsound results if they are analyzed context-insensitively. To set...

Unsoundness due to enabled region-offsets

1

This is the same scenario as in issue #1298. All analyses are set context-insensitively, and the sv-comp test `goblint-regression/06-symbeq_04-funloop_hard1.i` is analyzed with the `svcomp24` configuration. As stated in #1298 the...