search

Practical-Formal-Methods / adiff

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

unsound: ultimate + cpachecker #113

Closed chkl closed 6 years ago

chkl commented 6 years ago

from c/loop-acceleration/phases_false-unreach-call2_false-termination.i:

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
extern void __VERIFIER_assume(int);
extern unsigned int __VERIFIER_nondet_uint(void);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int main(void)
{
    unsigned int x = 1;
    unsigned int y = __VERIFIER_nondet_uint();
    if (!(y > 0))
    {
        return 0;
    }
    while (x < y)
    {
        if (x < y / x)
        {
            x *= x;
        }
        else
        {
            x++;
        }
    }
    __VERIFIER_assert(y != 120518 && y != 13 && y != 1924878313 && y != 1009745);
    __DUMMY_VERIFIER_assert(x != y);
}
chkl commented 6 years ago

Simplified:

extern void __VERIFIER_error() __attribute__((__noreturn__));
extern void __VERIFIER_assume(int);
extern unsigned int __VERIFIER_nondet_uint(void);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int main(void)
{
    unsigned int x = 1;
    unsigned int y = __VERIFIER_nondet_uint();
    if (!(y > 0))
    {
        return 0;
    }
    while (x < y)
    {
        if (x < y / x)
        {
            x *= x;
        }
        else
        {
            x++;
        }
    }
    __VERIFIER_assert(y != 13);
}

The while-loop is somehow essential for the bug to show and it is strangely present in cpachecker and ultimate.