diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 3a3fa7cdd..5091be08e 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -465,27 +465,27 @@ module ItvPure = struct | `Equal, `Equal -> `Equal | `NotComparable, _ | _, `NotComparable -> ( - match Bound.xcompare ~lhs:u1 ~rhs:l2 with - | `LeftSmallerThanRight -> + match (Bound.xcompare ~lhs:u1 ~rhs:l2, Bound.xcompare ~lhs:u2 ~rhs:l1) with + | `Equal, `Equal -> + `Equal (* weird, though *) + | (`Equal | `LeftSmallerThanRight), _ -> `LeftSmallerThanRight - | u1l2 -> ( - match (Bound.xcompare ~lhs:u2 ~rhs:l1, u1l2) with - | `LeftSmallerThanRight, _ -> - `RightSmallerThanLeft - | `Equal, `Equal -> - `Equal (* weird, though *) - | _, `Equal -> - `LeftSmallerThanRight - | _ -> - `NotComparable ) ) - | (`LeftSmallerThanRight | `Equal), (`LeftSmallerThanRight | `Equal) -> - `LeftSmallerThanRight - | (`RightSmallerThanLeft | `Equal), (`RightSmallerThanLeft | `Equal) -> - `RightSmallerThanLeft - | `LeftSmallerThanRight, `RightSmallerThanLeft -> - `LeftSubsumesRight + | _, (`Equal | `LeftSmallerThanRight) -> + `RightSmallerThanLeft + | (`NotComparable | `RightSmallerThanLeft), (`NotComparable | `RightSmallerThanLeft) -> + `NotComparable ) + | `Equal, `LeftSmallerThanRight + | `RightSmallerThanLeft, `Equal | `RightSmallerThanLeft, `LeftSmallerThanRight -> `RightSubsumesLeft + | `Equal, `RightSmallerThanLeft + | `LeftSmallerThanRight, `Equal + | `LeftSmallerThanRight, `RightSmallerThanLeft -> + `LeftSubsumesRight + | `LeftSmallerThanRight, `LeftSmallerThanRight -> + `LeftSmallerThanRight + | `RightSmallerThanLeft, `RightSmallerThanLeft -> + `RightSmallerThanLeft let join : t -> t -> t = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ea4fa0fed..006f4c580 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -69,7 +69,6 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_O codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Assignment,Binop: ([1, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 54d85acf3..cca301db4 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -69,8 +69,6 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Call,Call,Binop: (4 * [0, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Binop: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([1, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([2, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Binop: ([3, +oo] + 42):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Call,Call,Call,Assignment,Call,Call,Binop: (4 * [45, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 4fce9bacb..3fa9ddb15 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -147,7 +147,6 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 * (length.ub + -1)^2 + 8 * length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([10, +oo] + 1):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []