budget comparison

Comparing different budgets

Setup

Using random5.txt:

./c/array-examples/standard_copyInitSum2_false-unreach-call_ground.i
./c/reducercommutativity/sum40_true-unreach-call.i
./c/ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i
./c/array-industry-pattern/array_range_init_false-unreach-call.i
./c/loops/sum01_false-unreach-call_true-termination.i

By number of findings:

budget	unsound	incomplete	unsound-klee-cbmc-smack	disagreement
10	2	0	0	8
100	31	0	0	53
1000	346	1	5	286

by files:

budget	unsound	incomplete	unsound-klee-cbmc-smack	disagreement
10	2	0	0	4
100	4	0	0	4
1000	4	2	2	4

First of all: None found an unsoundness that was not caused by klee or smack.

One incompleteness by smack (5182c6c52294b348125db1907f841d3f272e327f)

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
int main()
{
    int a[100000];
    int b[100000];
    int i = 0;
    while (i < 100000)
    {
        a[i] = 42;
        i = i + 1;
    }
    __VERIFIER_assert(i != 10);
    for (i = 0; i < 100000; i++)
    {
        b[i] = a[i];
    }
    for (i = 0; i < 100000; i++)
    {
        a[i] = b[i] + i;
    }
    int x;
    for (x = 0; x < 100000; x++)
    {
        __DUMMY_VERIFIER_assert(b[x] == 42 + x);
    }
    return 0;
}

It looks really simple. This could really be a bug of Smack. So this case is the “incomplete” case and the 5 “unsound-klee-cbmc-smack” cases.

Addendum: What’s the minimum budget, required to find that case? This case has runId=5958, it is based on the first file in random5.txt, therefore the budget should be 5958 `div` 7 + 1 = 852.