@@ -5,13 +5,12 @@ import semmle.code.cpp.dataflow.DataFlow
5
5
6
6
/**
7
7
* Holds if the expression `e` assigns something including `va` to a
8
- * stack variable that is later null terminated at `e0`.
8
+ * stack variable `v0` that is later null terminated at `e0`.
9
9
*/
10
- private predicate mayAddNullTerminatorHelper ( Expr e , VariableAccess va , Expr e0 ) {
11
- exists ( StackVariable v0 , Expr val |
10
+ private predicate mayAddNullTerminatorHelper ( Expr e , VariableAccess va , StackVariable v0 ) {
11
+ exists ( Expr val |
12
12
exprDefinition ( v0 , e , val ) and // `e` is `v0 := val`
13
- val .getAChild * ( ) = va and
14
- mayAddNullTerminator ( e0 , v0 .getAnAccess ( ) )
13
+ val .getAChild * ( ) = va
15
14
)
16
15
}
17
16
@@ -47,8 +46,9 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
47
46
)
48
47
or
49
48
// Assignment to another stack variable
50
- exists ( Expr e0 |
51
- mayAddNullTerminatorHelper ( pragma [ only_bind_into ] ( e ) , va , pragma [ only_bind_into ] ( e0 ) ) and
49
+ exists ( StackVariable v0 , Expr e0 |
50
+ mayAddNullTerminatorHelper ( e , va , v0 ) and
51
+ mayAddNullTerminator ( pragma [ only_bind_into ] ( e0 ) , pragma [ only_bind_into ] ( v0 .getAnAccess ( ) ) ) and
52
52
controlFlowNodeSuccessorTransitive ( e , e0 )
53
53
)
54
54
or
0 commit comments