[inferbo] Assign unknown value for unknown functions

Reviewed By: mbouaziz

Differential Revision: D14363188

fbshipit-source-id: 5e7216dc1

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}
 

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -1,5 +1,4 @@
-../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==<std::allocator<char>_>, 10, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==<std::allocator<char>_>, 10, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+../../facebook-clang-plugins/clang/install/include/c++/v1/string, std::operator==<std::allocator<char>_>, 13, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::basic_string<char,std::char_traits<char>,std::allocator<char>>_data,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<Int_no_copy,std::allocator<Int_no_copy>>_erase, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Unknown value from: std::distance<std::__wrap_iter<const_Int_no_copy_*>_>,Binary operation: (this->infer_size - [-oo, +oo]):unsigned64]
 INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h, std::vector<int,std::allocator<int>>_insert<std::__list_iterator<int,_void_*>_>, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Unknown value from: std::distance<std::__list_iterator<int,_void_*>_>,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]