ty_mangled_name: only use non-mangled name if -Zcffi is enabled.

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -4,6 +4,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
 use cbmc::{InternString, InternedString};
+use kani_metadata::UnstableFeature;
 use rustc_abi::{
     BackendRepr::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
     TagEncoding, TyAndLayout, VariantIdx, Variants,
@@ -487,9 +488,20 @@ impl<'tcx> GotocCtx<'tcx> {
         // This is not a restriction because C can only access non-generic types anyway.
         // TODO: Skipping name mangling is likely insufficient if a dependent crate has two versions of
         // linked C libraries
-        // https://github.com/model-checking/kani/issues/450
+        // https://github.com/model-checking/kani/issues/450.
+        // Note that #[repr(C)] types are unmangled only if the unstable c-ffi feature is enabled; otherwise,
+        // we assume that this struct is a #[repr(C)] in Rust code and mangle it,
+        // c.f. https://github.com/model-checking/kani/issues/4007.
         match t.kind() {
-            TyKind::Adt(def, args) if args.is_empty() && def.repr().c() => {
+            TyKind::Adt(def, args)
+                if args.is_empty()
+                    && def.repr().c()
+                    && self
+                        .queries
+                        .args()
+                        .unstable_features
+                        .contains(&UnstableFeature::CFfi.to_string()) =>
+            {
                 // For non-generic #[repr(C)] types, use the literal path instead of mangling it.
                 self.tcx.def_path_str(def.did()).intern()
             }

tests/cargo-kani/dependency-test/dependency3/src/lib.rs

@@ -5,8 +5,18 @@ pub struct Foo {
     x: i32,
 }
 
+pub enum Field {
+    Case1,
+    Case2,
+}
+
+#[repr(C)]
+pub struct ReprCStruct {
+    pub field: Field,
+}
+
 // Export a function that takes a struct type which differs between this crate
-// and the other vesion
+// and the other version
 pub fn take_foo(foo: &Foo) -> i32 {
     foo.x
 }

tests/cargo-kani/dependency-test/diamond-dependency/dependency1/src/lib.rs

@@ -11,3 +11,7 @@ pub fn delegate_use_struct() -> i32 {
     let foo = dependency3::give_foo();
     dependency3::take_foo(&foo)
 }
+
+pub fn create_struct() -> dependency3::ReprCStruct {
+    dependency3::ReprCStruct { field: dependency3::Field::Case1 }
+}

tests/cargo-kani/dependency-test/diamond-dependency/dependency2/src/lib.rs

@@ -11,3 +11,7 @@ pub fn delegate_use_struct() -> i32 {
     let foo = dependency3::give_foo();
     dependency3::take_foo(&foo)
 }
+
+pub fn create_struct() -> dependency3::ReprCStruct {
+    dependency3::ReprCStruct { field: dependency3::Field::Case1 }
+}

tests/cargo-kani/dependency-test/diamond-dependency/dependency3/src/lib.rs

@@ -7,8 +7,18 @@ pub struct Foo {
     y: i32,
 }
 
+pub enum Field {
+    Case1,
+    Case2,
+}
+
+#[repr(C)]
+pub struct ReprCStruct {
+    pub field: Field,
+}
+
 // Export a function that takes a struct type which differs between this crate
-// and the other vesion.
+// and the other version.
 pub fn take_foo(foo: &Foo) -> i32 {
     foo.x + foo.y
 }

tests/cargo-kani/dependency-test/diamond-dependency/main/src/lib.rs

@@ -12,3 +12,11 @@ fn harness() {
     assert!(dependency1::delegate_use_struct() == 3);
     assert!(dependency2::delegate_use_struct() == 1);
 }
+
+// Test that Kani can codegen repr(C) structs from two different versions of the same crate,
+// c.f. https://github.com/model-checking/kani/issues/4007
+#[kani::proof]
+fn reprc_harness() {
+    dependency1::create_struct();
+    dependency2::create_struct();
+}