@@ -114,22 +114,40 @@ private predicate parseArgument(string arg, string s, int i, Opcode opcode) {
114114
115115private Element getAChildScope ( Element scope ) { result .getParentScope ( ) = scope }
116116
117+ pragma [ nomagic]
117118private predicate hasAVariable ( MacroInvocation mi , Stmt s , Element scope ) {
118119 assertion0 ( mi , s , _) and
119120 s .getParent ( ) = scope
120121 or
121122 hasAVariable ( mi , s , getAChildScope ( scope ) )
122123}
123124
124- private LocalScopeVariable getVariable ( MacroInvocation mi , int i ) {
125- exists ( string operand , string arg , Stmt s |
125+ private predicate hasParentScope ( Variable v , Element scope ) { v .getParentScope ( ) = scope }
126+
127+ pragma [ nomagic]
128+ private predicate hasAssertionOperand ( MacroInvocation mi , int i , Stmt s , string operand ) {
129+ exists ( string arg |
126130 assertion0 ( mi , s , arg ) and
127- parseArgument ( arg , operand , i , _) and
131+ parseArgument ( arg , operand , i , _)
132+ )
133+ }
134+
135+ pragma [ nomagic]
136+ private predicate hasNameAndParentScope ( string name , Element scope , Variable v ) {
137+ v .hasName ( name ) and
138+ hasParentScope ( v , scope )
139+ }
140+
141+ pragma [ nomagic]
142+ private LocalScopeVariable getVariable ( MacroInvocation mi , int i ) {
143+ exists ( string name , Stmt s |
144+ hasAssertionOperand ( mi , i , s , name ) and
128145 result =
129- unique( Variable v |
146+ unique( Variable v , Element parentScope |
147+ hasAssertionOperand ( mi , _, s , name ) and
130148 v .getLocation ( ) .getStartLine ( ) < s .getLocation ( ) .getStartLine ( ) and
131- hasAVariable ( mi , s , v . getParentScope ( ) ) and
132- v . hasName ( operand )
149+ hasAVariable ( mi , s , parentScope ) and
150+ hasNameAndParentScope ( name , parentScope , v )
133151 |
134152 v
135153 )
0 commit comments