@@ -5,13 +5,12 @@ import semmle.code.cpp.dataflow.DataFlow
55
66/**
77 * 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`.
99 */
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 |
1212 exprDefinition ( v0 , e , val ) and // `e` is `v0 := val`
13- val .getAChild * ( ) = va and
14- mayAddNullTerminator ( e0 , v0 .getAnAccess ( ) )
13+ val .getAChild * ( ) = va
1514 )
1615}
1716
@@ -47,8 +46,9 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
4746 )
4847 or
4948 // 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
5252 controlFlowNodeSuccessorTransitive ( e , e0 )
5353 )
5454 or
0 commit comments