Incorrectly labeled termination benchmarks in seq-mthreaded/
mchalupa opened this issue · 0 comments
mchalupa commented
These benchmarks from seq-mthreaded
directory seem to be incorrectly labeled w.r.t the no-termination property:
pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
pals_lcr.3_overflow.ufo.UNBOUNDED.pals.c
pals_lcr.5_overflow.ufo.UNBOUNDED.pals.c
pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c
pals_floodmax.3_overflow.ufo.UNBOUNDED.pals.c
pals_lcr.4_overflow.ufo.UNBOUNDED.pals.c
pals_opt-floodmax.3.2.ufo.UNBOUNDED.pals.c
pals_opt-floodmax.3_overflow.ufo.UNBOUNDED.pals.c
Although they have a while(1)
loop, this loop contains an assertion that eventually fails on every path. You can check that the loop is in fact bounded by instrumenting the programs with an explicit counter of the iterations and asserting that this counter has an upper bound, e.g.,:
diff --git a/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c b/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
index c80275cd00..37f69eb350 100644
--- a/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
+++ b/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
@@ -534,7 +534,9 @@ int main(void)
p32_old = nomsg;
p32_new = nomsg;
i2 = 0;
+ unsigned counter = 0;
while (1) {
+ assert(counter++ < 4);
{
node1();
node2();
@@ -552,7 +554,9 @@ int main(void)
p32_old = p32_new;
p32_new = nomsg;
c1 = check();
- assert(c1);
+ //assert(c1);
+ if (!c1)
+ abort();
}
}
}
The upper bounds (not all of them are tight) for the benchmarks are as follows:
benchmark | upper bound |
---|---|
pals_floodmax.3.3.ufo.UNBOUNDED.pals.c | 4 |
pals_lcr.3_overflow.ufo.UNBOUNDED.pals.c | 515 |
pals_lcr.5_overflow.ufo.UNBOUNDED.pals.c | 512 |
pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c | 4 |
pals_floodmax.3_overflow.ufo.UNBOUNDED.pals.c | 950 |
pals_lcr.4_overflow.ufo.UNBOUNDED.pals.c | 512 |
pals_opt-floodmax.3.2.ufo.UNBOUNDED.pals.c | 2 |
pals_opt-floodmax.3_overflow.ufo.UNBOUNDED.pals.c | 600 |
I checked that the assertions for upper bound hold with Symbiotic and CPAchecker (and some of the benchmarks also with other tools, e.g., CBMC with --unwinding-assertions or KLEE).