@@ -37,7 +37,6 @@ Stmt getPreviousStmt(Stmt s) {
3737 */
3838predicate firstUnreachableStmt ( Stmt s ) {
3939 not isReachable ( s ) and
40- not s instanceof EmptyStmt and
4140 (
4241 // a statement whose preceding statement in the same list is reachable
4342 isReachable ( getPreviousStmt ( s ) )
@@ -47,6 +46,16 @@ predicate firstUnreachableStmt(Stmt s) {
4746 )
4847}
4948
49+ /** Holds if `s` is in a run of unreachable statements following a constant condition. */
50+ predicate isInUnreachableRunAfterConstantCondition ( Stmt s ) {
51+ not isReachable ( s ) and
52+ (
53+ exists ( getPreviousStmt ( s ) .( IfStmt ) .getCondition ( ) .getBoolValue ( ) )
54+ or
55+ isInUnreachableRunAfterConstantCondition ( getPreviousStmt ( s ) )
56+ )
57+ }
58+
5059/**
5160 * Matches if `retval` is a constant or a struct composed wholly of constants.
5261 */
@@ -87,14 +96,32 @@ predicate allowlist(Stmt s) {
8796 exists ( ReturnStmt ret | ret = s |
8897 forall ( Expr retval | retval = ret .getAnExpr ( ) | isAllowedReturnValue ( retval ) )
8998 )
90- or
91- // statements deliberately made unreachable by a constant condition, such as the code
92- // following `if true { return }`
93- exists ( getPreviousStmt ( s ) .( IfStmt ) .getCondition ( ) .getBoolValue ( ) )
99+ }
100+
101+ /** Holds if `s` is part of a non-reportable prefix of a run of unreachable statements. */
102+ predicate isInNonReportableUnreachablePrefix ( Stmt s ) {
103+ ( allowlist ( s ) or s instanceof EmptyStmt ) and
104+ (
105+ firstUnreachableStmt ( s )
106+ or
107+ isInNonReportableUnreachablePrefix ( getPreviousStmt ( s ) )
108+ )
109+ }
110+
111+ /** Holds if `s` is the first non-allowlisted statement in a run of unreachable statements. */
112+ predicate firstNonAllowlistedUnreachableStmt ( Stmt s ) {
113+ not isReachable ( s ) and
114+ not s instanceof EmptyStmt and
115+ not allowlist ( s ) and
116+ (
117+ firstUnreachableStmt ( s )
118+ or
119+ isInNonReportableUnreachablePrefix ( getPreviousStmt ( s ) )
120+ )
94121}
95122
96123from Stmt s
97124where
98- firstUnreachableStmt ( s ) and
99- not allowlist ( s )
125+ firstNonAllowlistedUnreachableStmt ( s ) and
126+ not isInUnreachableRunAfterConstantCondition ( s )
100127select s , "This statement is unreachable."
0 commit comments