add expected tests

Author: thanhnguyen-aws

tests/expected/union/static_union.expected

@@ -0,0 +1,10 @@
+main.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: unsafe { FOO.a[1] } == 0"
+
+
+main.assertion.3\
+         - Status: SUCCESS\
+         - Description: "assertion failed: unsafe { BAR.b } == 3"\
+
+VERIFICATION:- SUCCESSFUL

tests/expected/union/static_union.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+static FOO: Data = Data { a: [0; 3] };
+
+static BAR: Data = Data { b: 3 };
+
+union Data {
+    a: [u8; 3],
+    b: u16,
+}
+
+#[kani::proof]
+fn main() {
+    let _x = &FOO;
+    assert!(unsafe { FOO.a[1] } == 0);
+    assert!(unsafe { BAR.b } == 3);
+}

tests/expected/union/static_union2.expected

@@ -0,0 +1,11 @@
+main.assertion.1\
+         - Status: SUCCESS\
+         - Description: "index out of bounds: the length is less than or equal to the given index"\
+
+Check 2: main.assertion.2\
+         - Status: FAILURE\
+         - Description: "assertion failed: unsafe { FOO.a[1] } == 5"\
+
+Failed Checks: assertion failed: unsafe { FOO.a[1] } == 5
+
+VERIFICATION:- FAILED

tests/expected/union/static_union2.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+static FOO: Data = Data { a: [0; 3] };
+
+union Data {
+    a: [u8; 3],
+    b: u16,
+}
+
+#[kani::proof]
+fn main() {
+    let _x = &FOO;
+    assert!(unsafe { FOO.a[1] } == 5);
+}

tests/expected/union/union_transmute.expected

@@ -0,0 +1,5 @@
+main.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: y == 256"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/union/union_transmute.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use std::mem::transmute;
+
+static FOO: Data = Data { a: [0, 1, 0] };
+
+#[derive(Copy, Clone)]
+union Data {
+    a: [u8; 3],
+    b: u16,
+}
+
+#[kani::proof]
+fn main() {
+    let y: u32 = unsafe { transmute(FOO) };
+    assert!(y == 256);
+}