@@ -3,11 +3,14 @@ private import semmle.code.cpp.models.interfaces.ArrayFunction
33private import semmle.code.cpp.models.implementations.Strcat
44import semmle.code.cpp.dataflow.DataFlow
55
6- private predicate mayAddNullTerminatorHelper ( Expr e , VariableAccess va , Expr e0 ) {
7- exists ( StackVariable v0 , Expr val |
8- exprDefinition ( v0 , e , val ) and
9- val .getAChild * ( ) = va and
10- mayAddNullTerminator ( e0 , v0 .getAnAccess ( ) )
6+ /**
7+ * Holds if the expression `e` assigns something including `va` to a
8+ * stack variable `v0`.
9+ */
10+ private predicate mayAddNullTerminatorHelper ( Expr e , VariableAccess va , StackVariable v0 ) {
11+ exists ( Expr val |
12+ exprDefinition ( v0 , e , val ) and // `e` is `v0 := val`
13+ val .getAChild * ( ) = va
1114 )
1215}
1316
@@ -25,8 +28,8 @@ private predicate controlFlowNodeSuccessorTransitive(ControlFlowNode n1, Control
2528}
2629
2730/**
28- * Holds if the expression `e` may add a null terminator to the string in
29- * variable `v `.
31+ * Holds if the expression `e` may add a null terminator to the string
32+ * accessed by `va `.
3033 */
3134predicate mayAddNullTerminator ( Expr e , VariableAccess va ) {
3235 // Assignment: dereferencing or array access
@@ -43,8 +46,9 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
4346 )
4447 or
4548 // Assignment to another stack variable
46- exists ( Expr e0 |
47- 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
4852 controlFlowNodeSuccessorTransitive ( e , e0 )
4953 )
5054 or
0 commit comments