Skip to content

Commit 144c345

Browse files
committed
disable cross-crate specs for unsafe core proof
1 parent e49dd1a commit 144c345

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

prusti/src/callbacks.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,12 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
156156
println!("{value}");
157157
}
158158
}
159-
CrossCrateSpecs::import_export_cross_crate(&mut env, &mut def_spec);
159+
160+
// FIXME: `prusti-std` has specs which unsafe core proof does not support
161+
if !config::unsafe_core_proof() {
162+
CrossCrateSpecs::import_export_cross_crate(&mut env, &mut def_spec);
163+
}
164+
160165
if !config::no_verify() {
161166
verify(env, def_spec);
162167
}

0 commit comments

Comments
 (0)