unsound crab: TODO

[chkl]

See pfm3.mpi-sws.org:8080/program/25454cc9ffdd2e2e7ec4e79df4312b62acafbefe

[wuestholz]

@chkl Yes, that looks like an unsoundness that I would report. Here's a minimized version:

extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int main()
{
    int i, j = 50, n = 5;
    __VERIFIER_assert((i <= n) != 0);
    return 0;
}

[chkl]

@wuestholz I think it's just because i is uninitialized. Not report-worthy then. (I only created the ticket while I was collecting numbers for the figures as a reminder to check it out later).

[wuestholz]

Ok, never mind then. I somehow read this as initializing both i and j. Seems to be a common misconception: https://stackoverflow.com/questions/6838408/how-can-i-declare-and-define-multiple-variables-in-one-line-using-c...