Skip to content

Commit 6c3455e

Browse files
committed
analyze: ignore !UNIQUE from pdg if --skip-borrowck is set
1 parent c7c5a2d commit 6c3455e

File tree

1 file changed

+6
-4
lines changed

1 file changed

+6
-4
lines changed

c2rust-analyze/src/analyze.rs

+6-4
Original file line numberDiff line numberDiff line change
@@ -785,6 +785,8 @@ fn run(tcx: TyCtxt) {
785785
}
786786
}
787787

788+
let skip_borrowck_everywhere = env::var("C2RUST_ANALYZE_SKIP_BORROWCK").as_deref() == Ok("1");
789+
788790
// Load permission info from PDG
789791
let pdg_compare = env::var("C2RUST_ANALYZE_COMPARE_PDG").as_deref() == Ok("1");
790792
// In compare mode, we load the PDG for comparison after analysis, not before.
@@ -796,6 +798,7 @@ fn run(tcx: TyCtxt) {
796798
&mut func_info,
797799
&mut asn,
798800
&mut updates_forbidden,
801+
skip_borrowck_everywhere,
799802
pdg_file_path,
800803
);
801804
}
@@ -877,8 +880,6 @@ fn run(tcx: TyCtxt) {
877880
debug!("=== ADT Metadata ===");
878881
debug!("{:?}", gacx.adt_metadata);
879882

880-
let skip_borrowck_everywhere = env::var("C2RUST_ANALYZE_SKIP_BORROWCK").as_deref() == Ok("1");
881-
882883
let mut loop_count = 0;
883884
loop {
884885
// Loop until the global assignment reaches a fixpoint. The inner loop also runs until a
@@ -2242,6 +2243,7 @@ fn pdg_update_permissions<'tcx>(
22422243
func_info: &mut HashMap<LocalDefId, FuncInfo<'tcx>>,
22432244
asn: &mut Assignment,
22442245
updates_forbidden: &mut GlobalPointerTable<PermissionSet>,
2246+
skip_borrowck_everywhere: bool,
22452247
pdg_file_path: impl AsRef<Path>,
22462248
) {
22472249
let allow_unsound =
@@ -2280,8 +2282,8 @@ fn pdg_update_permissions<'tcx>(
22802282
if node_info.flows_to.neg_offset.is_some() {
22812283
perms.insert(PermissionSet::OFFSET_SUB);
22822284
}
2283-
if !node_info.unique {
2284-
//perms.remove(PermissionSet::UNIQUE);
2285+
if !node_info.unique && !skip_borrowck_everywhere {
2286+
perms.remove(PermissionSet::UNIQUE);
22852287
}
22862288
}
22872289

0 commit comments

Comments
 (0)