Closed chkl closed 6 years ago
6df934f2e02ac78bb7f8887e8d2794da10c3c3ea (./c/ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i)
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(); } }
(But this is equal to the original SV-Comp benchmark)
This has also been fixed in the new version of cpachecker.
6df934f2e02ac78bb7f8887e8d2794da10c3c3ea
(./c/ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i
)(But this is equal to the original SV-Comp benchmark)