Infinite loop in counterexample check
The following program leads to a counterexample check that runs infinitely:
extern void __VERIFIER_error();
typedef struct {
char a;
} b;
typedef struct {
b c;
} d;
int e;
d f;
int main() {
char h;
e = h && f.c.a;
for (; ; )
if (e)
__VERIFIER_error();
}
Command line:
scripts/cpa.sh -valueAnalysis -spec sv-comp-reachability test.c -setprop log.consoleLevel=FINE
This also affects our SV-COMP configuration.
The counterexample that is checked is not large (cf. Counterexample.1.html), but somehow the counterexample check still never terminates. It just seems to endlessly create abstract states. Of course the automaton that the counterexample check uses to restrict the state space should prevent this.
(reported by Philipp Berger)