diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index e67b078ab..6f0d7c62f 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -64,7 +64,11 @@ module TransferFunctions = struct |> Dom.LatestPrune.subst ~ret_id eval_sym_trace location with | Ok latest_prune' -> - Dom.Mem.set_latest_prune latest_prune' mem + (* Note that we are losing some precisions here, e.g., the best results should be "and" of + caller's and callee's pruned conditions. For now, we defer the implementation of the + "and" since we haven't seen a case where "and" would help yet. *) + if Dom.LatestPrune.is_top latest_prune' then mem + else Dom.Mem.set_latest_prune latest_prune' mem | Error `SubstBottom -> Dom.Mem.bottom | Error `SubstFail -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index fbe308712..d72ee15a3 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -1121,6 +1121,8 @@ module LatestPrune = struct let top = Top + let is_top = function Top -> true | _ -> false + let forget locs = let is_mem_locs x = PowLoc.mem (Loc.of_pvar x) locs in function diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp index a74e2f96d..9bc49580e 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -202,3 +202,27 @@ void call_conditional_inequality_depth1_2_Good() { void call_conditional_inequality_depth1_3_Bad() { conditional_inequality_depth1(6); } + +class MyString { + char* _data = ""; + size_t _size = 0; + + public: + size_t size() { return _size; } + + char* data() { return _data; } +}; + +void set_fourth_idx(char* p) { p[3] = '0'; } + +void set_fourth_idx_safe(MyString* input) { + if (input->size() < 4) { + return; + } + set_fourth_idx(input->data()); +} + +void call_set_fourth_idx_safe_Good() { + MyString* s = new MyString(); + set_fourth_idx_safe(s); +}