Practical-Formal-Methods / adiff

Tool for differentially testing soundness and precision of program analyzers
MIT License
11 stars 6 forks source link

Super weird #100

Closed chkl closed 6 years ago

chkl commented 6 years ago

a90700e7e28ecc04d950081fb32c0c879e65f82e (./c/loops/eureka_05_true-unreach-call_true-termination.i)

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __DUMMY_VERIFIER_error();
    }
    return;
}
int array[5];
int n = 5;
void SelectionSort()
{
    int lh, rh, i, temp;
    for (lh = 0; lh < n; lh++)
    {
        rh = lh;
        for (i = lh + 1; i < n; i++)
            if (array[i] < array[rh])
            {
                rh = i;
            }
        temp = array[lh];
        array[lh] = array[rh];
        array[rh] = temp;
    }
}
int main(void)
{
    int array[5], i;
    __VERIFIER_assert(i != 1220141430);
    for (i = 5 - 1; i >= 0; i--)
        array[i] = i;
    SelectionSort();
    for (i = 0; i < 5; i++)
        __DUMMY_VERIFIER_assert(array[i] == i);
}
cbmc: Sat
rest : Unsat

what?

chkl commented 6 years ago

oh, instrumentation bug!