diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index f65cd5707..876a30d4c 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -26,9 +26,9 @@ type model = {exec: exec_fun; check: check_fun} let no_check _model_env _mem cond_set = cond_set let no_model = - let exec {pname} ~ret:_ mem = + let exec {pname; location} ~ret:(id, _) mem = L.d_printfln_escaped "No model for %a" Typ.Procname.pp pname ; - mem + Dom.Mem.add_unknown_from id ~callee_pname:pname ~location mem in {exec; check= no_check} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 9a363c2e8..63a1eda22 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,5 +1,4 @@ -../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==_>, 10, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==_>, 10, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==_>, 13, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: std::basic_string,std::allocator>_data,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this->infer_size`,,Unknown value from: std::distance_>,Binary operation: (this->infer_size - [-oo, +oo]):unsigned64] INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector>_insert_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Parameter `this->infer_size`,,Unknown value from: std::distance_>,Binary operation: (this->infer_size + [-oo, +oo]):unsigned64] codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow2_Good_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]