@@ -3,11 +3,14 @@ private import semmle.code.cpp.models.interfaces.ArrayFunction
3
3
private import semmle.code.cpp.models.implementations.Strcat
4
4
import semmle.code.cpp.dataflow.DataFlow
5
5
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
11
14
)
12
15
}
13
16
@@ -25,8 +28,8 @@ private predicate controlFlowNodeSuccessorTransitive(ControlFlowNode n1, Control
25
28
}
26
29
27
30
/**
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 `.
30
33
*/
31
34
predicate mayAddNullTerminator ( Expr e , VariableAccess va ) {
32
35
// Assignment: dereferencing or array access
@@ -43,8 +46,9 @@ predicate mayAddNullTerminator(Expr e, VariableAccess va) {
43
46
)
44
47
or
45
48
// 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
48
52
controlFlowNodeSuccessorTransitive ( e , e0 )
49
53
)
50
54
or
0 commit comments