Skip to content

Commit 567eeaa

Browse files
committed
[inferbo] Fix an ignored case when the upper bounds of offset is +oo, and the upper bound of size is smaller than +oo
Summary: The buffer overrun checker misses to handle the case when the upper bound of offset is +oo, and the upper bound of array size is less than +oo, which will causes false negative in some test cases. For instance, for the following program, ``` int a[1]; for(int i=0; a[i]; i++) {} ``` The variable `i` will eventually be equal 1 and causes an overrun error within the loop statement. However, this error was missed by buffer overrun checker.
1 parent 9dac096 commit 567eeaa

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -347,6 +347,10 @@ module ArrayAccessCondition = struct
347347
Bound.is_not_infty (ItvPure.ub real_idx) && Bound.le (ItvPure.ub size) (ItvPure.ub real_idx)
348348
then {report_issue_type= Issue IssueType.buffer_overrun_l2; propagate= false}
349349
(* symbolic il >= sl, probably an error *)
350+
else if
351+
Bound.is_infty (ItvPure.ub real_idx) && Bound.is_not_infty (ItvPure.ub size)
352+
then {report_issue_type= Issue IssueType.buffer_overrun_l3; propagate= false}
353+
(* su < iu = +oo, probably an error *)
350354
else if
351355
Bound.is_symbolic (ItvPure.lb real_idx) && Bound.le (ItvPure.lb size) (ItvPure.lb real_idx)
352356
then {report_issue_type= Issue IssueType.buffer_overrun_s2; propagate= true}

0 commit comments

Comments
 (0)