Fixing manes used by contracts metadata

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -7,7 +7,7 @@ use crate::args::ReachabilityType;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::analysis;
 use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
-use crate::kani_middle::metadata::gen_test_metadata;
+use crate::kani_middle::metadata::{canonical_mangled_name, gen_test_metadata};
 use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
  collect_reachable_items, filter_const_crate_items, filter_crate_items,
@@ -255,7 +255,7 @@ impl CodegenBackend for GotocCodegenBackend {
  self.queries
  .lock()
  .unwrap()
- .add_modifies_contract(harness.name().intern(), assigns_contract);
+ .add_modifies_contract(canonical_mangled_name(harness).intern(), assigns_contract);
  }
  }
  }

kani-compiler/src/kani_middle/metadata.rs

@@ -14,15 +14,19 @@ use stable_mir::CrateDef;
 
 use super::{attributes::KaniAttributes, SourceLocation};
 
+pub fn canonical_mangled_name(instance: Instance) -> String {
+ let pretty_name = instance.name();
+ // Main function a special case in order to support `--function main`
+ // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
+ if pretty_name == "main" { pretty_name } else { instance.mangled_name() }
+}
+
 /// Create the harness metadata for a proof harness for a given function.
 pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
  let def = instance.def;
  let attributes = KaniAttributes::for_instance(tcx, instance).harness_attributes();
  let pretty_name = instance.name();
- // Main function a special case in order to support `--function main`
- // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
- let mangled_name =
- if pretty_name == "main" { pretty_name.clone() } else { instance.mangled_name() };
+ let mangled_name = canonical_mangled_name(instance);
 
  // We get the body span to include the entire function definition.
  // This is required for concrete playback to properly position the generated test.