@@ -1247,13 +1247,14 @@ private predicate storeCand2(Content f, boolean stored, Configuration conf) {
12471247
12481248/**
12491249 * Holds if `f` is the target of both a store and a read in the path graph
1250- * covered by `nodeCand2`. `apNonEmpty` indiciates whether some access path
1251- * before the store (and after the read) is non-empty.
1250+ * covered by `nodeCand2`.
12521251 */
12531252pragma [ noinline]
1254- private predicate readStoreCand ( Content f , boolean apNonEmpty , Configuration conf ) {
1255- storeCand2 ( f , apNonEmpty , conf ) and
1256- readCand2 ( f , apNonEmpty , conf )
1253+ private predicate readStoreCand ( Content f , Configuration conf ) {
1254+ exists ( boolean apNonEmpty |
1255+ storeCand2 ( f , apNonEmpty , conf ) and
1256+ readCand2 ( f , apNonEmpty , conf )
1257+ )
12571258}
12581259
12591260private predicate nodeCand2 ( NodeExt node , Configuration config ) { nodeCand2 ( node , _, _, config ) }
@@ -1392,30 +1393,20 @@ private module LocalFlowBigStep {
13921393
13931394private import LocalFlowBigStep
13941395
1395- pragma [ nomagic]
1396- private predicate readExtCand2_0 ( Content f , NodeExt node1 , NodeExt node2 , Configuration config ) {
1397- readExt ( node1 , f , node2 , config ) and
1398- nodeCand2 ( node1 , _, true , config )
1399- }
1400-
14011396pragma [ nomagic]
14021397private predicate readExtCand2 ( NodeExt node1 , Content f , NodeExt node2 , Configuration config ) {
1403- readExtCand2_0 ( f , node1 , node2 , config ) and
1398+ readExt ( node1 , f , node2 , config ) and
1399+ nodeCand2 ( node1 , _, true , unbind ( config ) ) and
14041400 nodeCand2 ( node2 , config ) and
1405- readStoreCand ( f , _, unbind ( config ) )
1406- }
1407-
1408- pragma [ nomagic]
1409- private predicate storeExtCand2_0 ( Content f , NodeExt node1 , NodeExt node2 , Configuration config ) {
1410- storeExt ( node1 , f , node2 , config ) and
1411- nodeCand2 ( node1 , config )
1401+ readStoreCand ( f , unbind ( config ) )
14121402}
14131403
14141404pragma [ nomagic]
14151405private predicate storeExtCand2 ( NodeExt node1 , Content f , NodeExt node2 , Configuration config ) {
1416- storeExtCand2_0 ( f , node1 , node2 , config ) and
1417- nodeCand2 ( node2 , _, true , config ) and
1418- readStoreCand ( f , _, unbind ( config ) )
1406+ storeExt ( node1 , f , node2 , config ) and
1407+ nodeCand2 ( node1 , config ) and
1408+ nodeCand2 ( node2 , _, true , unbind ( config ) ) and
1409+ readStoreCand ( f , unbind ( config ) )
14191410}
14201411
14211412private newtype TAccessPathFront =
@@ -2031,7 +2022,6 @@ private predicate readFwd(
20312022
20322023pragma [ nomagic]
20332024private predicate flowConsCand ( Content f , AccessPath ap , Configuration config ) {
2034- flowConsCandFwd ( f , _, ap , unbind ( config ) ) and
20352025 exists ( NodeExt n , NodeExt mid |
20362026 flow ( mid , _, ap , config ) and
20372027 readFwd ( n , f , mid , _, ap , config )
0 commit comments