Decision #169 — library/core/src/ptr/mod.rs:1921
Status: partial
Truth table
| row | c0 br 1105 | c1 br 1106 | c2 br 1114 | c3 br 1115 | c4 br 1371 | c5 br 1403 | c6 br 1404 | outcome |
|---|---|---|---|---|---|---|---|---|
| 6468 | * | * | * | * | * | T | * | T |
| 6469 | * | * | * | * | * | T | * | T |
| 6470 | * | * | * | * | * | T | * | T |
| 6471 | * | * | F | * | F | F | F | F |
| 6472 | * | * | * | * | * | F | F | F |
| 43665 | * | * | F | * | F | F | F | F |
| 43666 | * | * | F | * | F | F | F | F |
| 43667 | * | * | * | * | * | F | F | F |
| 47118 | * | * | F | * | F | F | F | F |
| 47119 | * | * | F | * | F | F | F | F |
| 47120 | * | * | * | * | * | F | F | F |
| 131201 | * | * | F | * | F | F | F | F |
| 132528 | * | * | F | * | F | F | F | F |
Independent-effect pairs
c0(branch1105): DEAD view gap →scry_analyze_core::run_taint_analysis· br_if
inlined: lib.rs:4991 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c1(branch1106): DEAD view gap →scry_analyze_core::run_taint_analysis· br_if
inlined: lib.rs:4991 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c2(branch1114): GAP view gap →scry_analyze_core::run_taint_analysis· br_if
inlined: lib.rs:5015 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c3(branch1115): DEAD view gap →scry_analyze_core::run_taint_analysis· br_if
inlined: lib.rs:5015 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c4(branch1371): GAP view gap →scry_analyze_core::run_taint_analysis· br_if
inlined: lib.rs:5085 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c5(branch1403): PROVED — pair rows6468,6471(masking)scry_analyze_core::run_taint_analysis· br_if
inlined: lib.rs:2155 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c6(branch1404): GAP view gap →scry_analyze_core::run_taint_analysis· br_if
inlined: lib.rs:2155 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045