From f5789d09cb34d50cb86d37f8f570c419e1b0be2d Mon Sep 17 00:00:00 2001 From: Jim Grundy <85949519+jimgrundy@users.noreply.github.com> Date: Fri, 26 Nov 2021 16:17:23 -0600 Subject: [PATCH] Fixed typos --- regression/contracts/function_check_mem_01/main.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c index a743d9362f7..924cb723c5e 100644 --- a/regression/contracts/function_check_mem_01/main.c +++ b/regression/contracts/function_check_mem_01/main.c @@ -9,7 +9,7 @@ #define __CPROVER_VALID_MEM(ptr, size) \ __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \ - !__CPROVER_invalid_pointer((ptr)) && \ + !__CPROVER_is_invalid_pointer((ptr)) && \ __CPROVER_POINTER_OBJECT((ptr)) != \ __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \ __CPROVER_POINTER_OBJECT((ptr)) != \ @@ -28,7 +28,7 @@ void foo(bar *x) __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar))) { x->x += 1; - return + return; } int main()