We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
2 parents 8a720e0 + f5789d0 commit 0d62ff5Copy full SHA for 0d62ff5
regression/contracts/function_check_mem_01/main.c
@@ -9,7 +9,7 @@
9
10
#define __CPROVER_VALID_MEM(ptr, size) \
11
__CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \
12
- !__CPROVER_invalid_pointer((ptr)) && \
+ !__CPROVER_is_invalid_pointer((ptr)) && \
13
__CPROVER_POINTER_OBJECT((ptr)) != \
14
__CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
15
@@ -28,7 +28,7 @@ void foo(bar *x)
28
__CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
29
{
30
x->x += 1;
31
- return
+ return;
32
}
33
34
int main()
0 commit comments