1+
2+ ┌─ 1 (root, init)
3+ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+ │ span: src/rust/library/std/src/rt.rs:194
5+ │
6+ │ (61 steps)
7+ ├─ 3 (split)
8+ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
9+ │ function: eats_struct_args
10+ ┃
11+ ┃ (branch)
12+ ┣━━┓ subst: .Subst
13+ ┃ ┃ constraint:
14+ ┃ ┃ notBool ARG_INT2:Int ==Int ARG_INT5:Int
15+ ┃ │
16+ ┃ ├─ 4
17+ ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
18+ ┃ │ function: eats_struct_args
19+ ┃ │
20+ ┃ │ (96 steps)
21+ ┃ ├─ 6 (split)
22+ ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) )
23+ ┃ │ function: eats_struct_args
24+ ┃ ┃
25+ ┃ ┃ (branch)
26+ ┃ ┣━━┓ subst: .Subst
27+ ┃ ┃ ┃ constraint:
28+ ┃ ┃ ┃ ARG_UINT3:Int ==Int ARG_UINT6:Int
29+ ┃ ┃ │
30+ ┃ ┃ ├─ 8
31+ ┃ ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) )
32+ ┃ ┃ │ function: eats_struct_args
33+ ┃ ┃ │
34+ ┃ ┃ │ (6 steps)
35+ ┃ ┃ └─ 10 (stuck, leaf)
36+ ┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
37+ ┃ ┃ span: no-location:0
38+ ┃ ┃
39+ ┃ ┗━━┓ subst: .Subst
40+ ┃ ┃ constraint:
41+ ┃ ┃ notBool ARG_UINT3:Int ==Int ARG_UINT6:Int
42+ ┃ │
43+ ┃ ├─ 9
44+ ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) )
45+ ┃ │ function: eats_struct_args
46+ ┃ │
47+ ┃ │ (6 steps)
48+ ┃ ├─ 11 (terminal)
49+ ┃ │ #EndProgram ~> .K
50+ ┃ │ function: eats_struct_args
51+ ┃ │
52+ ┃ ┊ constraint: true
53+ ┃ ┊ subst: ...
54+ ┃ └─ 2 (leaf, target, terminal)
55+ ┃ #EndProgram ~> .K
56+ ┃
57+ ┗━━┓ subst: .Subst
58+ ┃ constraint:
59+ ┃ ARG_INT2:Int ==Int ARG_INT5:Int
60+ │
61+ ├─ 5
62+ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
63+ │ function: eats_struct_args
64+ │
65+ │ (66 steps)
66+ ├─ 7 (terminal)
67+ │ #EndProgram ~> .K
68+ │ function: eats_struct_args
69+ │
70+ ┊ constraint: true
71+ ┊ subst: ...
72+ └─ 2 (leaf, target, terminal)
73+ #EndProgram ~> .K
74+
75+
76+
77+
78+ STATISTICS
79+ -----------
80+ Total nodes: 10
81+
82+ Node roles (exclusive):
83+ target : 1 ids: 2
84+ terminal: 2 ids: 7, 11
85+ failing : 1 ids: 10
86+ split : 2 ids: 3, 6
87+ normal : 4 ids: 4, 5, 8, 9
88+ (root nodes omitted from totals: 1)
89+
90+ Leaf paths from init:
91+ total leaves (non-root): 2
92+ reachable leaves : 2
93+ total steps : 290
94+
95+ leaf 2 (path 1/2): steps 127, path 1 -> 3 -> 5 -> 7 -> 2
96+ leaf 2 (path 2/2): steps 163, path 1 -> 3 -> 4 -> 6 -> 9 -> 11 -> 2
97+ leaf 10: steps 163, path 1 -> 3 -> 4 -> 6 -> 8 -> 10
98+
99+ LEAF <k> CELLS
100+ ---------------
101+ Node 2:
102+ #EndProgram ~> .K
103+
104+ Node 10:
105+ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>E" ) , id: defId ( 27 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x008\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 0 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) ) .Operands , span ( 65 ) ) ~> .K
106+ >> function: core::panicking::panic::h<hash>
107+ >> call span: <REPO>/kmir/src/tests/integration/data/prove-rs/symbolic-structs-fail.rs:29:5
0 commit comments