cpachecker: (function called with reference modifies variable)

[chkl]

1366385b22aa0f11d0eb94f69febec711976a513

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();
    }
}
void err()
{
ERROR:
    __DUMMY_VERIFIER_error();
}
void mutex_lock(int * a)
{
    if (*a == 1)
    {
        err();
    }
    *a = 1;
}
void mutex_unlock(int * b)
{
    if (*b != 1)
    {
        err();
    }
    *b = 0;
}
int main()
{
    int m;
    m = 0;
    mutex_lock(&m);
    __VERIFIER_assert(m != 1);
    mutex_unlock(&m);
}

(This is a clear case, but might have been caught by SV-Comp already) TODO: Check SV-Comp

[chkl]

Similarly 6df934f2e02ac78bb7f8887e8d2794da10c3c3ea (./c/ldv-regression/alias_of_return_true-termination.c_true-unreach-call.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:
        __VERIFIER_error();
    }
}
void err()
{
    __DUMMY_VERIFIER_error();
}
int * return_self(int * p)
{
    return p;
}
int main()
{
    int a, * q;
    a = 1;
    q = return_self(&a);
    *q = 2;
    __VERIFIER_assert(a != 2 != 0);
    if (a != 2)
    {
        err();
    }
}

[chkl]

This bug is already fixed in the latest version of cpachecker.