diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 81009fb99..f84d04a2d 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -204,6 +204,11 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s || Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre else Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre then (inv_map, ReachedFixPoint) + else if is_narrowing && not (Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) then ( + L.(debug Analysis Verbose) + "Terminate narrowing because old and new states are not comparable at %a:%a@." + Typ.Procname.pp (Procdesc.get_proc_name pdesc) Node.pp_id node_id ; + (inv_map, ReachedFixPoint) ) else let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in update_inv_map new_pre ~visit_count:visit_count' diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 439d90f4a..e3e56c06f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -186,4 +186,5 @@ codetoanalyze/c/bufferoverrun/unreachable.c, condition_always_true_with_else_bad codetoanalyze/c/bufferoverrun/unreachable.c, infinite_loop_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/unreachable.c, never_loops_bad, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/unreachable.c, unreachable_statement_exit_bad, 1, UNREACHABLE_CODE, no_bucket, ERROR, [] +codetoanalyze/c/bufferoverrun/while_loop.c, diverge_on_narrowing, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c index 8dd76f5a0..ae5a98443 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c @@ -13,3 +13,17 @@ void while_loop() { while (*(a + i) && i < 10) /* BUG */ a[i++] = 1; /* SAFE */ } + +struct S { + struct S* f; +}; + +void dummy_func(struct S* x) {} + +void diverge_on_narrowing() { + struct S* x; + while (1) { + dummy_func(0); + x = x->f; + } +}