@@ -16,6 +16,11 @@ private module Cached {
16
16
LoadStep ( TypeTrackerContentSet contents ) or
17
17
JumpStep ( )
18
18
19
+ pragma [ nomagic]
20
+ private TypeTracker noContentTypeTracker ( boolean hasCall ) {
21
+ result = MkTypeTracker ( hasCall , noContent ( ) )
22
+ }
23
+
19
24
/** Gets the summary resulting from appending `step` to type-tracking summary `tt`. */
20
25
cached
21
26
TypeTracker append ( TypeTracker tt , StepSummary step ) {
@@ -28,21 +33,24 @@ private module Cached {
28
33
or
29
34
step = ReturnStep ( ) and hasCall = false and result = tt
30
35
or
31
- exists ( TypeTrackerContentSet contents |
32
- step = LoadStep ( contents ) and
33
- currentContent = contents .getAReadContent ( ) and
34
- result = MkTypeTracker ( hasCall , noContent ( ) )
35
- )
36
- or
37
- exists ( TypeTrackerContentSet contents |
38
- step = StoreStep ( contents ) and
39
- currentContent = noContent ( ) and
40
- result = MkTypeTracker ( hasCall , contents .getAStoreContent ( ) )
41
- )
42
- or
43
36
step = JumpStep ( ) and
44
37
result = MkTypeTracker ( false , currentContent )
45
38
)
39
+ or
40
+ exists ( TypeTrackerContentSet contents , boolean hasCall |
41
+ step = LoadStep ( pragma [ only_bind_into ] ( contents ) ) and
42
+ tt = MkTypeTracker ( hasCall , contents .getAReadContent ( ) ) and
43
+ result = noContentTypeTracker ( hasCall )
44
+ or
45
+ step = StoreStep ( pragma [ only_bind_into ] ( contents ) ) and
46
+ tt = noContentTypeTracker ( hasCall ) and
47
+ result = MkTypeTracker ( hasCall , contents .getAStoreContent ( ) )
48
+ )
49
+ }
50
+
51
+ pragma [ nomagic]
52
+ private TypeBackTracker noContentTypeBackTracker ( boolean hasReturn ) {
53
+ result = MkTypeBackTracker ( hasReturn , noContent ( ) )
46
54
}
47
55
48
56
/** Gets the summary resulting from prepending `step` to this type-tracking summary. */
@@ -57,21 +65,19 @@ private module Cached {
57
65
or
58
66
step = ReturnStep ( ) and result = MkTypeBackTracker ( true , content )
59
67
or
60
- exists ( TypeTrackerContentSet contents |
61
- step = LoadStep ( contents ) and
62
- content = noContent ( ) and
63
- result = MkTypeBackTracker ( hasReturn , contents .getAStoreContent ( ) )
64
- )
65
- or
66
- exists ( TypeTrackerContentSet contents |
67
- step = StoreStep ( contents ) and
68
- content = contents .getAReadContent ( ) and
69
- result = MkTypeBackTracker ( hasReturn , noContent ( ) )
70
- )
71
- or
72
68
step = JumpStep ( ) and
73
69
result = MkTypeBackTracker ( false , content )
74
70
)
71
+ or
72
+ exists ( TypeTrackerContentSet contents , boolean hasReturn |
73
+ step = StoreStep ( pragma [ only_bind_into ] ( contents ) ) and
74
+ tbt = MkTypeBackTracker ( hasReturn , contents .getAReadContent ( ) ) and
75
+ result = noContentTypeBackTracker ( hasReturn )
76
+ or
77
+ step = LoadStep ( pragma [ only_bind_into ] ( contents ) ) and
78
+ tbt = noContentTypeBackTracker ( hasReturn ) and
79
+ result = MkTypeBackTracker ( hasReturn , contents .getAStoreContent ( ) )
80
+ )
75
81
}
76
82
77
83
/**
0 commit comments