==> is not short circuited #6319
Description
CBMC version: develop (currently @ e32a83f)
Operating system: Linux
Test case:
#include <assert.h>
#include <stdbool.h>
#include <stdlib.h>
int main() {
int *c = NULL;
// --pointer-check raises a FAILURE here, but assertion passes
assert(false ==> *c == 0);
// --pointer-check raises no failure, and assertion passes
assert(!false || *c == 0);
// --pointer-check raises no failure, and assertion passes
if(false) assert(*c == 0);
// --pointer-check raises no failure, and assertion passes
__CPROVER_assume(false);
assert(*c == 0);
}Exact command line resulting in the issue:
$ cbmc bug.c --pointer-check
[... snip ...]
** Results:
bug.c function main
[main.assertion.1] line 9 assertion false ==> *c == 0: SUCCESS
[main.pointer_dereference.1] line 9 dereference failure: pointer NULL in *c: FAILURE
[main.assertion.2] line 12 assertion !false || *c == 0: SUCCESS
[main.pointer_dereference.2] line 12 dereference failure: pointer NULL in *c: SUCCESS
[main.assertion.3] line 15 assertion *c == 0: SUCCESS
[main.pointer_dereference.3] line 15 dereference failure: pointer NULL in *c: SUCCESS
[main.assertion.4] line 19 assertion *c == 0: SUCCESS
[main.pointer_dereference.4] line 19 dereference failure: pointer NULL in *c: SUCCESS
** 1 of 8 failed (2 iterations)
VERIFICATION FAILEDAlthough the assertion false ==> *c == 0 is marked SUCCESS, CBMC reports a spurious pointer deref failure in *c.
What behaviour did you expect:
a ==> b should be short circuited and should behave the same way as !a || b. In this particular case, b should not be checked for pointer deref issues if a is not satisfied.