Decision #88 — library/core/src/ptr/mod.rs:1939
Status: partial
Truth table
| row | c0 br 474 | c1 br 501 | c2 br 502 | c3 br 503 | c4 br 504 | outcome |
|---|---|---|---|---|---|---|
| 66 | T | * | * | * | * | T |
| 7026 | T | * | * | * | * | T |
| 13764 | T | * | * | * | * | T |
| 21193 | T | * | * | * | * | T |
| 23936 | T | * | * | * | * | T |
| 26579 | T | * | * | * | * | T |
| 29430 | T | * | * | * | * | T |
| 50285 | T | * | * | * | * | T |
| 70969 | T | * | * | * | * | T |
| 80852 | T | * | * | * | * | T |
| 90709 | T | * | * | * | * | T |
| 98483 | T | * | * | * | * | T |
| 106977 | T | * | * | * | * | T |
| 115053 | T | * | * | * | * | T |
| 122907 | T | * | * | * | * | T |
| 139626 | T | * | * | * | * | T |
| 156304 | T | * | * | * | * | T |
| 166162 | T | * | * | * | * | T |
| 175951 | T | * | * | * | * | T |
| 180749 | T | * | * | * | * | T |
| 184069 | T | * | * | * | * | T |
| 187176 | T | * | * | * | * | T |
| 190520 | T | F | F | F | F | F |
| 190521 | * | F | F | T | * | T |
| 194776 | T | F | F | F | F | F |
| 194777 | * | F | F | F | T | T |
| 194778 | * | F | F | F | F | F |
| 194779 | * | F | F | F | T | T |
| 194780 | * | F | F | F | F | F |
| 194781 | * | F | F | F | T | T |
| 202850 | T | F | F | T | * | T |
| 206126 | T | F | F | F | F | F |
| 206127 | * | F | F | T | * | T |
| 206128 | * | F | F | T | * | T |
| 206129 | * | F | F | F | T | T |
| 206130 | * | F | F | F | F | F |
| 206131 | * | F | F | T | * | T |
| 206132 | * | F | F | T | * | T |
| 206133 | * | F | F | F | T | T |
| 214482 | T | F | F | F | F | F |
| 214483 | * | F | F | F | T | T |
| 222038 | T | * | * | * | * | T |
| 299415 | T | * | * | * | * | T |
| 376706 | T | * | * | * | * | T |
| 379343 | T | * | * | * | * | T |
| 382227 | T | * | * | * | * | T |
Independent-effect pairs
All 5 conditions live in <core::iter::adapters::map::Map<core::slice::iter::Iter<scry_analyze_core::DefinedFunc>, scry_analyze_core::compute_stack_usage::{closure#0}> as core::iter::traits::iterator::Iterator>::fold::<(), core::iter::traits::iterator::Iterator::for_each::call<scry_analyze_core::StackBound, <alloc::vec::Vec<scry_analyze_core::StackBound>>::extend_trusted<core::iter::adapters::map::Map<core::slice::iter::Iter<scry_analyze_core::DefinedFunc>, scry_analyze_core::compute_stack_usage::{closure#0}>>::{closure#0}>::{closure#0}> — 5 br_if
c0(branch474): GAP view gap →c1(branch501): GAP view gap →c2(branch502): GAP view gap →c3(branch503): PROVED — pair rows190520,190521(masking)c4(branch504): PROVED — pair rows190520,194777(masking)