@@ -834,6 +834,7 @@ private predicate localFlowExit(Node node, Configuration config) {
834
834
* This is the transitive closure of `[additional]localFlowStep` beginning
835
835
* at `localFlowEntry`.
836
836
*/
837
+ pragma [ nomagic]
837
838
private predicate localFlowStepPlus (
838
839
Node node1 , Node node2 , boolean preservesValue , Configuration config
839
840
) {
@@ -1094,28 +1095,44 @@ private predicate flowCand0(Node node, boolean toReturn, AccessPathFront apf, Co
1094
1095
flowCandFwd ( node , _, apf , config )
1095
1096
)
1096
1097
or
1097
- exists ( Node mid , Content f , AccessPathFront apf0 |
1098
- store ( node , f , mid ) and
1099
- flowCand ( mid , toReturn , apf0 , config ) and
1098
+ exists ( Content f , AccessPathFront apf0 |
1099
+ flowCandStore ( node , f , toReturn , apf0 , config ) and
1100
1100
apf0 .headUsesContent ( f ) and
1101
1101
consCand ( f , apf , unbind ( config ) )
1102
1102
)
1103
1103
or
1104
- exists ( Node mid , Content f , AccessPathFront apf0 |
1105
- read ( node , f , mid ) and
1106
- flowCand ( mid , toReturn , apf0 , config ) and
1104
+ exists ( Content f , AccessPathFront apf0 |
1105
+ flowCandRead ( node , f , toReturn , apf0 , config ) and
1107
1106
consCandFwd ( f , apf0 , unbind ( config ) ) and
1108
1107
apf .headUsesContent ( f )
1109
1108
)
1110
1109
}
1111
1110
1111
+ pragma [ nomagic]
1112
+ private predicate flowCandRead (
1113
+ Node node , Content f , boolean toReturn , AccessPathFront apf0 , Configuration config
1114
+ ) {
1115
+ exists ( Node mid |
1116
+ read ( node , f , mid ) and
1117
+ flowCand ( mid , toReturn , apf0 , config )
1118
+ )
1119
+ }
1120
+
1121
+ private predicate flowCandStore (
1122
+ Node node , Content f , boolean toReturn , AccessPathFront apf0 , Configuration config
1123
+ ) {
1124
+ exists ( Node mid |
1125
+ store ( node , f , mid ) and
1126
+ flowCand ( mid , toReturn , apf0 , config )
1127
+ )
1128
+ }
1129
+
1112
1130
private predicate consCand ( Content f , AccessPathFront apf , Configuration config ) {
1113
1131
consCandFwd ( f , apf , config ) and
1114
- exists ( Node mid , Node n , AccessPathFront apf0 |
1132
+ exists ( Node n , AccessPathFront apf0 |
1115
1133
flowCandFwd ( n , _, apf0 , config ) and
1116
1134
apf0 .headUsesContent ( f ) and
1117
- read ( n , f , mid ) and
1118
- flowCand ( mid , _, apf , config )
1135
+ flowCandRead ( n , f , _, apf , config )
1119
1136
)
1120
1137
}
1121
1138
0 commit comments