Fix expected test output files

model-checking · Jul 29, 2024 · 0f11c95 · 0f11c95
1 parent 08494ed
commit 0f11c95
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 100 deletions.
diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected
@@ -1,56 +1,38 @@
-Checking harness delayed_ub_slices...
+delayed_ub_slices.assertion.4\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`"
 
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`
+delayed_ub_structs.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`"
 
-VERIFICATION:- FAILED
+delayed_ub_copy.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-Checking harness delayed_ub_structs...
+delayed_ub_closure_capture_laundered.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `U`
+delayed_ub_closure_laundered.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-VERIFICATION:- FAILED
+delayed_ub_laundered.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-Checking harness delayed_ub_copy...
+delayed_ub_static.assertion.4\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
+delayed_ub_transmute.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-VERIFICATION:- FAILED
-
-Checking harness delayed_ub_closure_capture_laundered...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
-
-VERIFICATION:- FAILED
-
-Checking harness delayed_ub_closure_laundered...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
-
-VERIFICATION:- FAILED
-
-Checking harness delayed_ub_laundered...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
-
-VERIFICATION:- FAILED
-
-Checking harness delayed_ub_static...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
-
-VERIFICATION:- FAILED
-
-Checking harness delayed_ub_transmute...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
-
-VERIFICATION:- FAILED
-
-Checking harness delayed_ub...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
-
-VERIFICATION:- FAILED
+delayed_ub.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
 Summary:
 Verification failed for - delayed_ub_slices

diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected
@@ -1,68 +1,46 @@
-Checking harness check_typed_swap_safe...
+std::ptr::read::<std::mem::MaybeUninit<u8>>.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>."
 
-Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>.
+std::ptr::read::<std::mem::MaybeUninit<u8>>.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>."
 
-Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>.
+std::ptr::write::<std::mem::MaybeUninit<u8>>.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>."
 
-VERIFICATION:- FAILED
+std::ptr::write::<std::mem::MaybeUninit<u8>>.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>."
 
-Checking harness check_typed_swap...
+check_typed_swap.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`"
 
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`
+check_typed_swap.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`"
 
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`
+check_volatile_load.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>.
+check_compare_bytes.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `std::mem::MaybeUninit<u8>.
+check_compare_bytes.assertion.2\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-VERIFICATION:- FAILED
+std::intrinsics::copy::<u8>.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
-Checking harness check_volatile_store_and_load_safe...
-
-VERIFICATION:- SUCCESSFUL
-
-Checking harness check_volatile_load...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
-
-VERIFICATION:- FAILED
-
-Checking harness check_write_bytes_safe...
-
-VERIFICATION:- SUCCESSFUL
-
-Checking harness check_compare_bytes_safe...
-
-VERIFICATION:- SUCCESSFUL
-
-Checking harness check_compare_bytes...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
-
-VERIFICATION:- FAILED
-
-Checking harness check_copy_safe...
-
-VERIFICATION:- SUCCESSFUL
-
-Checking harness check_copy...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
-
-VERIFICATION:- FAILED
-
-Checking harness check_copy_nonoverlapping_safe...
-
-VERIFICATION:- SUCCESSFUL
-
-Checking harness check_copy_nonoverlapping...
-
-Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
-
-VERIFICATION:- FAILED
+std::intrinsics::copy_nonoverlapping::<u8>.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`"
 
 Summary:
 Verification failed for - check_typed_swap_safe