From aee7a04aa0b4d9b3638a9a22ede0983d8e16c9cc Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sat, 19 Oct 2024 12:10:24 -0500 Subject: [PATCH] Update test small_slice_eq --- .../expected/loop-contract/small_slice_eq.rs | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/tests/expected/loop-contract/small_slice_eq.rs b/tests/expected/loop-contract/small_slice_eq.rs index a59436122da5..31ae9da8c640 100644 --- a/tests/expected/loop-contract/small_slice_eq.rs +++ b/tests/expected/loop-contract/small_slice_eq.rs @@ -6,20 +6,25 @@ // Modifications Copyright Kani Contributors // See GitHub history for details. -// kani-flags: -Z loop-contracts --enable-unstable --cbmc-args --arrays-uf-always --no-standard-checks --object-bits 8 +// kani-flags: -Z loop-contracts -Z mem-predicates --enable-unstable --cbmc-args --object-bits 8 -//! Check if loop contracts are correctly applied. The flag --no-standard-checks should be -//! removed once same_object predicate is supported in loop contracts. +//! Check if loop contracts are correctly applied. #![feature(stmt_expr_attributes)] #![feature(proc_macro_hygiene)] #![feature(ptr_sub_ptr)] + +extern crate kani; + +use kani::mem::same_allocation; + unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { debug_assert_eq!(x.len(), y.len()); unsafe { let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); - #[kani::loop_invariant( px as isize >= x.as_ptr() as isize + #[kani::loop_invariant( same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) + && px as isize >= x.as_ptr() as isize && py as isize >= y.as_ptr() as isize && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] while px < pxend { @@ -43,9 +48,10 @@ fn small_slice_eq_harness() { // because DFCC contract enforcement assumes that a definition for `free` // exists. let _ = Box::new(10); - let mut a = [1; 2000]; - let mut b = [1; 2000]; + const ARR_SIZE: usize = 2000; + let x: [u8; ARR_SIZE] = kani::any(); + let y: [u8; ARR_SIZE] = kani::any(); unsafe { - small_slice_eq(&mut a, &mut b); + small_slice_eq(&x, &y); } }