Practical-Formal-Methods / adiff

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

unsigned int: weird #106

Closed chkl closed 6 years ago

chkl commented 6 years ago

Based on 79df55f351e0c6c23990075cf43b0cdc3032b5cb:

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();
    while (x < y)
    {
        x *= x;
    }
    __VERIFIER_assert(y != 3);
}

results:

cpachecker, seacrab, seahorn, uautomizer, utaipan: unsat
rest: unknown

I am quite confused, this seems super simple.