@@ -73,19 +73,30 @@ extensible predicate restrictAlertsToExactLocation(
7373
7474/** Module for applying alert location filtering. */
7575module AlertFilteringImpl< LocationSig Location> {
76+ pragma [ nomagic]
77+ private predicate restrictAlertsToEntireFile ( string filePath ) { restrictAlertsTo ( filePath , 0 , 0 ) }
78+
79+ pragma [ nomagic]
80+ private predicate restrictAlertsToStartLine ( string filePath , int line ) {
81+ exists ( int startLineStart , int startLineEnd |
82+ restrictAlertsTo ( filePath , startLineStart , startLineEnd ) and
83+ line = [ startLineStart .. startLineEnd ]
84+ )
85+ }
86+
7687 /** Applies alert filtering to the given location. */
7788 bindingset [ location]
7889 predicate filterByLocation ( Location location ) {
7990 not restrictAlertsTo ( _, _, _) and not restrictAlertsToExactLocation ( _, _, _, _, _)
8091 or
81- exists ( string filePath , int startLineStart , int startLineEnd |
82- restrictAlertsTo ( filePath , startLineStart , startLineEnd )
83- |
84- startLineStart = 0 and
85- startLineEnd = 0 and
92+ exists ( string filePath |
93+ restrictAlertsToEntireFile ( filePath ) and
8694 location .hasLocationInfo ( filePath , _, _, _, _)
8795 or
88- location .hasLocationInfo ( filePath , [ startLineStart .. startLineEnd ] , _, _, _)
96+ exists ( int line |
97+ restrictAlertsToStartLine ( filePath , line ) and
98+ location .hasLocationInfo ( filePath , line , _, _, _)
99+ )
89100 )
90101 or
91102 exists ( string filePath , int startLine , int startColumn , int endLine , int endColumn |
0 commit comments