Add test for issue model-checking#560.

tests/kani/PhantomData/phantom_fixme.rs

@@ -0,0 +1,42 @@
+// compile-flags: --edition 2018
+// cbmc-flags: --unwind 4 --object-bits 9
+//
+// Testcase based on https://doc.rust-lang.org/rust-by-example/generics/phantom/testcase_units.html
+// which reproduces issue https://github.com/model-checking/kani/issues/560
+
+use std::marker::PhantomData;
+use std::ops::Add;
+
+#[derive(Debug, Clone, Copy)]
+enum Mm {}
+
+/// `Length` is a type with phantom type parameter `Unit`,
+/// and is not generic over the length type (that is `u32`).
+///
+/// `u32` already implements the `Clone` and `Copy` traits.
+#[derive(Debug, Clone, Copy)]
+struct Length<Unit>(u32, PhantomData<Unit>);
+
+/// The `Add` trait defines the behavior of the `+` operator.
+impl<Unit> Add for Length<Unit> {
+    type Output = Length<Unit>;
+
+    // add() returns a new `Length` struct containing the sum.
+    fn add(self, rhs: Length<Unit>) -> Length<Unit> {
+        // `+` calls the `Add` implementation for `u32`.
+        Length(self.0 + rhs.0, PhantomData)
+    }
+}
+
+fn main() {
+    // `one_meter` has phantom type parameter `Mm`.
+    let one_meter: Length<Mm> = Length(1000, PhantomData);
+
+    // `+` calls the `add()` method we implemented for `Length<Unit>`.
+    //
+    // Since `Length` implements `Copy`, `add()` does not consume
+    // `one_foot` and `one_meter` but copies them into `self` and `rhs`.
+    let two_meters = one_meter + one_meter;
+
+    assert!(two_meters.0 == 2000);
+}