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.
1 parent 8a720e0 commit f5789d0Copy full SHA for f5789d0
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