@@ -75,19 +75,30 @@ extensible predicate restrictAlertsToExactLocation(
75
75
76
76
/** Module for applying alert location filtering. */
77
77
module AlertFilteringImpl< LocationSig Location> {
78
+ pragma [ nomagic]
79
+ private predicate restrictAlertsToEntireFile ( string filePath ) { restrictAlertsTo ( filePath , 0 , 0 ) }
80
+
81
+ pragma [ nomagic]
82
+ private predicate restrictAlertsToStartLine ( string filePath , int line ) {
83
+ exists ( int startLineStart , int startLineEnd |
84
+ restrictAlertsTo ( filePath , startLineStart , startLineEnd ) and
85
+ line = [ startLineStart .. startLineEnd ]
86
+ )
87
+ }
88
+
78
89
/** Applies alert filtering to the given location. */
79
90
bindingset [ location]
80
91
predicate filterByLocation ( Location location ) {
81
92
not restrictAlertsTo ( _, _, _) and not restrictAlertsToExactLocation ( _, _, _, _, _)
82
93
or
83
- exists ( string filePath , int startLineStart , int startLineEnd |
84
- restrictAlertsTo ( filePath , startLineStart , startLineEnd )
85
- |
86
- startLineStart = 0 and
87
- startLineEnd = 0 and
94
+ exists ( string filePath |
95
+ restrictAlertsToEntireFile ( filePath ) and
88
96
location .hasLocationInfo ( filePath , _, _, _, _)
89
97
or
90
- location .hasLocationInfo ( filePath , [ startLineStart .. startLineEnd ] , _, _, _)
98
+ exists ( int line |
99
+ restrictAlertsToStartLine ( filePath , line ) and
100
+ location .hasLocationInfo ( filePath , line , _, _, _)
101
+ )
91
102
)
92
103
or
93
104
exists ( string filePath , int startLine , int startColumn , int endLine , int endColumn |
0 commit comments