diff --git a/rust-tests/cbmc-reg/FatPointers/boxslice1.rs b/rust-tests/cbmc-reg/FatPointers/boxslice1.rs
new file mode 100644
index 000000000000..61da693cc879
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/boxslice1.rs
@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Casts boxed array to boxed slice (example taken from rust documentation)
+use std::str;
+
+fn main() {
+    // This vector of bytes is used to initialize a Box<[u8; 4]>
+    let sparkle_heart_vec = vec![240, 159, 146, 150];
+
+    // This transformer produces a Box<[u8>]
+    let _sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
+
+    // see boxslice2_fail.rs for an attempt to test sparkle_heart_str
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs b/rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs
new file mode 100644
index 000000000000..87a54c8f9316
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs
@@ -0,0 +1,23 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Casts boxed array to boxed slice (example taken from rust documentation)
+use std::str;
+
+fn main() {
+    // This vector of bytes is used to initialize a Box<[u8; 4]>
+    let sparkle_heart_vec = vec![240, 159, 146, 150];
+
+    // This transformer produces a Box<[u8>]
+    let sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
+
+    // This match statement generates failures even though
+    // the binary runs without failures.
+    match sparkle_heart_str {
+        Ok(string) => match string.bytes().nth(0) {
+            Some(b) => assert!(b == 240),
+            _ => assert!(true),
+        },
+        _ => assert!(true),
+    }
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/boxtrait.rs b/rust-tests/cbmc-reg/FatPointers/boxtrait.rs
new file mode 100644
index 000000000000..13bc7f45be2f
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/boxtrait.rs
@@ -0,0 +1,34 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This is handled by the box to box case of unsized pointers
+
+pub trait Trait {
+    fn increment(&mut self);
+    fn get(&self) -> u32;
+}
+
+struct Concrete {
+    pub index: u32,
+}
+
+impl Concrete {
+    fn new() -> Self {
+        Concrete { index: 0 }
+    }
+}
+
+impl Trait for Concrete {
+    fn increment(&mut self) {
+        self.index = self.index + 1;
+    }
+    fn get(&self) -> u32 {
+        self.index
+    }
+}
+
+fn main() {
+    let mut x: Box<dyn Trait> = Box::new(Concrete::new());
+    x.increment();
+    assert!(x.get() == 1);
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/slice1.rs b/rust-tests/cbmc-reg/FatPointers/slice1.rs
new file mode 100644
index 000000000000..c43a48a76bc1
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/slice1.rs
@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let array = [1, 2, 3, 4, 5, 6];
+    let slice: &[u32] = &array;
+    assert!(slice[0] == 1);
+    assert!(slice[5] == 6);
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/slice2.rs b/rust-tests/cbmc-reg/FatPointers/slice2.rs
new file mode 100644
index 000000000000..569e8ecf4739
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/slice2.rs
@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let array = [1, 2, 3, 4, 5, 6];
+    let slice = &array[2..5];
+    assert!(slice[0] == 3);
+    assert!(slice[2] == 5);
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/slice3.rs b/rust-tests/cbmc-reg/FatPointers/slice3.rs
new file mode 100644
index 000000000000..5f08278cf019
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/slice3.rs
@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let array = [1, 2, 3, 4, 5, 6];
+    let slice1 = &array[2..5];
+    let slice2 = &slice1[1..2];
+    assert!(slice2[0] == 4);
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/structslice.rs b/rust-tests/cbmc-reg/FatPointers/structslice.rs
new file mode 100644
index 000000000000..d424bd742df2
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/structslice.rs
@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+struct Concrete {
+    array: [u32; 4],
+}
+
+struct Abstract<'a> {
+    uints: &'a [u32],
+}
+
+fn main() {
+    let x = Concrete { array: [1, 2, 3, 4] };
+    assert!(x.array[0] == 1);
+    let y = Abstract { uints: &[10, 11, 12, 13] };
+    assert!(y.uints[0] == 10);
+    assert!(y.uints[3] == 13);
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/trait1.rs b/rust-tests/cbmc-reg/FatPointers/trait1.rs
new file mode 100644
index 000000000000..2eec16094a26
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/trait1.rs
@@ -0,0 +1,31 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Cast a concrete ref to a trait ref.
+
+pub trait Subscriber {
+    fn process(&self) -> u32;
+}
+
+struct DummySubscriber {
+    val: u32,
+}
+
+impl DummySubscriber {
+    fn new() -> Self {
+        DummySubscriber { val: 0 }
+    }
+}
+
+impl Subscriber for DummySubscriber {
+    fn process(&self) -> u32 {
+        let DummySubscriber { val: v } = self;
+        *v + 1
+    }
+}
+
+fn main() {
+    let _d = DummySubscriber::new();
+    let _s = &_d as &dyn Subscriber;
+    assert!(_s.process() == 1);
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/trait2.rs b/rust-tests/cbmc-reg/FatPointers/trait2.rs
new file mode 100644
index 000000000000..2ca1638adb0b
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/trait2.rs
@@ -0,0 +1,31 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Cast a concrete ref to a trait raw pointer.
+
+pub trait Subscriber {
+    fn process(&self) -> u32;
+}
+
+struct DummySubscriber {
+    val: u32,
+}
+
+impl DummySubscriber {
+    fn new() -> Self {
+        DummySubscriber { val: 0 }
+    }
+}
+
+impl Subscriber for DummySubscriber {
+    fn process(&self) -> u32 {
+        let DummySubscriber { val: v } = self;
+        *v + 1
+    }
+}
+
+fn main() {
+    let _d = DummySubscriber::new();
+    let _s = &_d as *const dyn Subscriber;
+    assert!(unsafe { _s.as_ref().unwrap().process() } == 1);
+}
diff --git a/rust-tests/cbmc-reg/FatPointers/trait3.rs b/rust-tests/cbmc-reg/FatPointers/trait3.rs
new file mode 100644
index 000000000000..4d9feeb2e443
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/trait3.rs
@@ -0,0 +1,45 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Cast a concrete ref to
+//   concrete raw pointer
+//   trait ref
+//   trait raw pointer
+// Cast a trait ref to a trait raw pointer
+
+pub trait Subscriber {
+    fn process(&self) -> u32;
+}
+
+struct DummySubscriber {
+    val: u32,
+}
+
+impl DummySubscriber {
+    fn new() -> Self {
+        DummySubscriber { val: 0 }
+    }
+}
+
+impl Subscriber for DummySubscriber {
+    fn process(&self) -> u32 {
+        let DummySubscriber { val: v } = self;
+        *v + 1
+    }
+}
+
+fn main() {
+    let d = DummySubscriber::new();
+
+    let d1 = &d as *const DummySubscriber;
+    assert!(unsafe { d1.as_ref().unwrap().process() } == 1);
+
+    let s = &d as &dyn Subscriber;
+    assert!(s.process() == 1);
+
+    let s1 = &d as *const dyn Subscriber;
+    assert!(unsafe { s1.as_ref().unwrap().process() } == 1);
+
+    let x = s as *const dyn Subscriber;
+    assert!(unsafe { x.as_ref().unwrap().process() } == 1);
+}
diff --git a/rust-tests/cbmc-reg/Transparent/transparent1.rs b/rust-tests/cbmc-reg/Transparent/transparent1.rs
new file mode 100644
index 000000000000..96386187c4ad
--- /dev/null
+++ b/rust-tests/cbmc-reg/Transparent/transparent1.rs
@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    let mut x: u32 = 4;
+    let pointer0: std::ptr::NonNull<u32> = std::ptr::NonNull::new(&mut x).unwrap();
+    let y = unsafe { *pointer0.as_ptr() };
+    assert!(y == 4);
+}
diff --git a/rust-tests/cbmc-reg/Transparent/transparent2.rs b/rust-tests/cbmc-reg/Transparent/transparent2.rs
new file mode 100644
index 000000000000..d872cad4ccdf
--- /dev/null
+++ b/rust-tests/cbmc-reg/Transparent/transparent2.rs
@@ -0,0 +1,36 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[derive(Clone, Copy)]
+struct Target {
+    x: u32,
+    y: u32,
+}
+
+struct Container<T> {
+    ptr: std::ptr::NonNull<T>,
+}
+
+impl<T> Container<T>
+where
+    T: Copy,
+{
+    fn new(val: &mut T) -> Self {
+        return Container { ptr: std::ptr::NonNull::new(val).unwrap() };
+    }
+    fn get(&self) -> T {
+        return unsafe { *self.ptr.as_ptr() };
+    }
+}
+
+fn main() {
+    let mut x: u32 = 4;
+    let container = Container::new(&mut x);
+    let _y = container.get();
+    assert_eq!(_y, 4);
+
+    let mut target: Target = Target { x: 3, y: 4 };
+    let cont = Container::new(&mut target);
+    assert!((unsafe { *cont.ptr.as_ptr() }).x == 3);
+    assert!((unsafe { *cont.ptr.as_ptr() }).y == 4);
+}
diff --git a/rust-tests/cbmc-reg/Transparent/transparent3.rs b/rust-tests/cbmc-reg/Transparent/transparent3.rs
new file mode 100644
index 000000000000..7d342118bdeb
--- /dev/null
+++ b/rust-tests/cbmc-reg/Transparent/transparent3.rs
@@ -0,0 +1,20 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//#repr(transparent)]
+pub struct Pointer<T> {
+    pointer: *const T,
+}
+
+pub struct Container<T> {
+    container: Pointer<T>,
+}
+
+fn main() {
+    let x: u32 = 4;
+    let my_pointer = Pointer { pointer: &x };
+    let my_container = Container { container: my_pointer };
+
+    let y: u32 = unsafe { *my_container.container.pointer };
+    assert!(y == 4);
+}
diff --git a/rust-tests/cbmc-reg/Transparent/transparent4.rs b/rust-tests/cbmc-reg/Transparent/transparent4.rs
new file mode 100644
index 000000000000..96c1916858c5
--- /dev/null
+++ b/rust-tests/cbmc-reg/Transparent/transparent4.rs
@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[repr(transparent)]
+pub struct Pointer<T> {
+    pointer: *const T,
+}
+
+#[repr(transparent)]
+pub struct Wrapper<T>(T);
+
+pub struct Container<T> {
+    container: Pointer<T>,
+}
+
+fn main() {
+    let x: u32 = 4;
+    let my_container = Container { container: Pointer { pointer: &x } };
+
+    let y: u32 = unsafe { *my_container.container.pointer };
+    assert!(y == 4);
+
+    let w: Wrapper<u32> = Wrapper(4);
+
+    let Wrapper(c) = w;
+    assert!(c == 4);
+}