More tests and test fixes

tests/expected/uninit/unions.expected

@@ -1,12 +1,17 @@
-union_complex_subfields.assertion.1\
+union_update_should_fail.assertion.1\
 	 - Status: FAILURE\
-	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`"\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
+
+union_complex_subfields_should_fail.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`"
 
-basic_union_fail.assertion.1\
+basic_union_should_fail.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
 
 Summary:
-Verification failed for - union_complex_subfields
-Verification failed for - basic_union_fail
-Complete - 2 successfully verified harnesses, 2 failures, 4 total.
+Verification failed for - union_update_should_fail
+Verification failed for - union_complex_subfields_should_fail
+Verification failed for - basic_union_should_fail
+Complete - 3 successfully verified harnesses, 3 failures, 6 total.

tests/expected/uninit/unions.rs

@@ -35,9 +35,16 @@ union U1 {
     b: (u32, u16, u8),
 }
 
-/// Tests accessing uninit data via subfields of a union.
+/// Tests accessing initialized data via subfields of a union.
 #[kani::proof]
 unsafe fn union_complex_subfields_should_pass() {
+    let u = U1 { a: (0, 0) };
+    let non_padding = u.b.0;
+}
+
+/// Tests accessing uninit data via subfields of a union.
+#[kani::proof]
+unsafe fn union_complex_subfields_should_fail() {
     let u = U1 { a: (0, 0) };
     let non_padding = u.b.1;
 }
@@ -49,3 +56,11 @@ unsafe fn union_update_should_pass() {
     u.b = 0;
     let non_padding = u.b;
 }
+
+/// Tests overwriting data inside unions.
+#[kani::proof]
+unsafe fn union_update_should_fail() {
+    let mut u = U { a: 0 };
+    u.a = 0;
+    let non_padding = u.b;
+}