@@ -84,14 +84,19 @@ predicate pointerArithOverflow0(
84
84
pai .getElementSize ( ) = f .getUnspecifiedType ( ) .( ArrayType ) .getBaseType ( ) .getSize ( ) and
85
85
f .getUnspecifiedType ( ) .( ArrayType ) .getArraySize ( ) = size and
86
86
semBounded ( getSemanticExpr ( pai .getRight ( ) ) , any ( SemZeroBound b ) , bound , true , _) and
87
- delta = bound - size
87
+ delta = bound - size and
88
+ delta >= 0 and
89
+ size != 0 and
90
+ size != 1
88
91
}
89
92
90
93
module PointerArithmeticToDerefConfig implements DataFlow:: ConfigSig {
91
94
predicate isSource ( DataFlow:: Node source ) {
92
95
pointerArithOverflow0 ( source .asInstruction ( ) , _, _, _, _)
93
96
}
94
97
98
+ predicate isBarrierIn ( DataFlow:: Node node ) { isSource ( node ) }
99
+
95
100
predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink1 ( sink , _, _) }
96
101
}
97
102
@@ -127,18 +132,17 @@ module FieldAddressToDerefConfig implements DataFlow::StateConfigSig {
127
132
128
133
predicate isBarrier ( DataFlow:: Node node , FlowState state ) { none ( ) }
129
134
135
+ predicate isBarrierIn ( DataFlow:: Node node ) { isSource ( node , _) }
136
+
130
137
predicate isAdditionalFlowStep (
131
138
DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
132
139
) {
133
- exists ( PointerArithmeticInstruction pai , Field f , int size , int delta |
140
+ exists ( PointerArithmeticInstruction pai , Field f |
134
141
state1 = TArray ( f ) and
135
142
state2 = TOverflowArithmetic ( pai ) and
136
143
pai .getLeft ( ) = node1 .asInstruction ( ) and
137
144
node2 .asInstruction ( ) = pai and
138
- pointerArithOverflow ( pai , f , size , _, delta ) and
139
- delta >= 0 and
140
- size != 0 and
141
- size != 1
145
+ pointerArithOverflow ( pai , f , _, _, _)
142
146
)
143
147
}
144
148
}
0 commit comments