Closed
Description
CBMC version: develop
Operating system: Mac OS 10.15.7
Test case:
#include <assert.h>
#include <stdbool.h>
#include <stdlib.h>
bool validate(const char *data, unsigned allocated)
{
bool check_1 = (data == NULL ==> allocated == 0);
bool check_2 = (allocated != 0 ==> __CPROVER_r_ok(data, allocated));
return check_1 && check_2;
}
void main()
{
char *data;
unsigned allocated;
data = (allocated == 0) ? NULL : malloc(allocated);
__CPROVER_assume(validate(data, allocated));
assert(validate(data, allocated));
}Exact command line resulting in the issue:
Either cbmc --smt2 test.c or cbmc --cprover-smt2 test.c.
[Note that z3 is required with the --smt2 flag.]
What behaviour did you expect:
Same behaviour as without the --smt2 flag -- CBMC should be able to establish the assertion.
What happened instead:
CBMC fails to verify the assertion.
$ cbmc test.c | tail
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS
test.c function main
[main.assertion.1] line 21 assertion validate(data, allocated): SUCCESS
** 0 of 3 failed (1 iterations)
VERIFICATION SUCCESSFUL
$ cbmc --smt2 test.c | tail
** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS
test.c function main
[main.assertion.1] line 21 assertion validate(data, allocated): FAILURE
** 1 of 3 failed (2 iterations)
VERIFICATION FAILED