@@ -75,19 +75,30 @@ extensible predicate restrictAlertsToExactLocation(
7575
7676/** Module for applying alert location filtering. */
7777module 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+
7889 /** Applies alert filtering to the given location. */
7990 bindingset [ location]
8091 predicate filterByLocation ( Location location ) {
8192 not restrictAlertsTo ( _, _, _) and not restrictAlertsToExactLocation ( _, _, _, _, _)
8293 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
8896 location .hasLocationInfo ( filePath , _, _, _, _)
8997 or
90- location .hasLocationInfo ( filePath , [ startLineStart .. startLineEnd ] , _, _, _)
98+ exists ( int line |
99+ restrictAlertsToStartLine ( filePath , line ) and
100+ location .hasLocationInfo ( filePath , line , _, _, _)
101+ )
91102 )
92103 or
93104 exists ( string filePath , int startLine , int startColumn , int endLine , int endColumn |
0 commit comments