@@ -33,6 +33,7 @@ private predicate stmtCandidate(Stmt s) {
3333pragma [ nomagic]
3434private predicate macroInvocationLocation ( int startline , Function f , MacroInvocation mi ) {
3535 mi .getMacroName ( ) = [ "assert" , "__analysis_assume" ] and
36+ mi .getNumberOfArguments ( ) = 1 and
3637 mi .getLocation ( ) .hasLocationInfo ( _, startline , _, _, _) and
3738 f .getEntryPoint ( ) .isAffectedByMacro ( mi )
3839}
@@ -49,7 +50,7 @@ private predicate stmtParentLocation(int startline, Function f, StmtParent p) {
4950 * is the only thing on the line.
5051 */
5152pragma [ nomagic]
52- private predicate assertion0 ( MacroInvocation mi , Stmt s ) {
53+ private predicate assertion0 ( MacroInvocation mi , Stmt s , string arg ) {
5354 stmtCandidate ( s ) and
5455 s =
5556 unique( StmtParent p , int startline , Function f |
@@ -61,12 +62,13 @@ private predicate assertion0(MacroInvocation mi, Stmt s) {
6162 not p = mi .getAnExpandedElement ( )
6263 |
6364 p
64- )
65+ ) and
66+ arg = mi .getUnexpandedArgument ( 0 )
6567}
6668
6769private Function getEnclosingFunctionForMacroInvocation ( MacroInvocation mi ) {
6870 exists ( Stmt s |
69- assertion0 ( mi , s ) and
71+ assertion0 ( mi , s , _ ) and
7072 result = s .getEnclosingFunction ( )
7173 )
7274}
@@ -110,11 +112,28 @@ private predicate parseArgument(string arg, string s, int i, Opcode opcode) {
110112 opcode instanceof Opcode:: CompareEQ
111113}
112114
113- /** Gets a local variable named `s` in `f`. */
114- pragma [ nomagic]
115- private LocalScopeVariable getAVariableWithNameInFunction ( Function f , string s ) {
116- result .getName ( ) = s and
117- result .getFunction ( ) = f
115+ private Element getAChildScope ( Element scope ) { result .getParentScope ( ) = scope }
116+
117+ private predicate hasAVariable ( MacroInvocation mi , Stmt s , Element scope ) {
118+ assertion0 ( mi , s , _) and
119+ s .getParent ( ) = scope
120+ or
121+ hasAVariable ( mi , s , getAChildScope ( scope ) )
122+ }
123+
124+ private LocalScopeVariable getVariable ( MacroInvocation mi , int i ) {
125+ exists ( string operand , string arg , Stmt s |
126+ assertion0 ( mi , s , arg ) and
127+ parseArgument ( arg , operand , i , _) and
128+ result =
129+ unique( Variable v |
130+ v .getLocation ( ) .getStartLine ( ) < s .getLocation ( ) .getStartLine ( ) and
131+ hasAVariable ( mi , s , v .getParentScope ( ) ) and
132+ v .hasName ( operand )
133+ |
134+ v
135+ )
136+ )
118137}
119138
120139/**
@@ -126,7 +145,7 @@ private predicate hasVarAccessMacroArgument(MacroInvocation mi, Variable var, in
126145 arg = mi .getUnexpandedArgument ( 0 ) and
127146 f = getEnclosingFunctionForMacroInvocation ( mi ) and
128147 parseArgument ( arg , s , i , opcode ) and
129- var = unique ( | | getAVariableWithNameInFunction ( f , s ) )
148+ var = getVariable ( mi , i )
130149 )
131150}
132151
@@ -136,8 +155,7 @@ private predicate hasVarAccessMacroArgument(MacroInvocation mi, Variable var, in
136155 */
137156private predicate hasConstMacroArgument ( MacroInvocation mi , int k , int i , Opcode opcode ) {
138157 exists ( string arg , string s |
139- assertion0 ( mi , _) and
140- arg = mi .getUnexpandedArgument ( 0 ) and
158+ assertion0 ( mi , _, arg ) and
141159 s .toInt ( ) = k and
142160 parseArgument ( arg , s , i , opcode )
143161 )
@@ -160,7 +178,7 @@ private predicate hasAssertionOpcode(MacroInvocation mi, Opcode opcode) {
160178 * in the control-flow graph at `s`.
161179 */
162180predicate assertion ( MacroInvocation mi , Stmt s ) {
163- assertion0 ( mi , s ) and
181+ assertion0 ( mi , s , _ ) and
164182 hasAssertionOperand ( mi , 0 ) and
165183 hasAssertionOperand ( mi , 1 )
166184}
0 commit comments