From 118295e03c23a5031ec0457ba3b9521df57db7f7 Mon Sep 17 00:00:00 2001 From: Andrzej Kotulski Date: Fri, 15 Jul 2016 05:39:50 -0700 Subject: [PATCH] Fix C++ models of c library Summary: When analyzing C model in C++, we were seeing some SKIP function triggered by generated constructors/operators= for C structs. In C they weren't present, but in C++ compiler generates them for us. To avoid this (and future) problems with models, translate all functions that are needed when computing the model Reviewed By: dulmarod Differential Revision: D3561873 fbshipit-source-id: f8ad2a0 --- infer/models/c/src/libc_basic.c | 20 ++++++++++++++++--- infer/src/clang/cLocation.ml | 3 ++- .../cpp/errors/c_tests/c_bugs.cpp | 18 +++++++++++++++++ infer/tests/endtoend/cpp/CBugsTest.java | 19 ++++++++++++++++++ 4 files changed, 56 insertions(+), 4 deletions(-) diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c index 826ab7bfa..d3af81da7 100644 --- a/infer/models/c/src/libc_basic.c +++ b/infer/models/c/src/libc_basic.c @@ -30,18 +30,32 @@ #include "infer_builtins.h" -#include +// use c++ headers if in C++ mode - they are mostly same as C headers, +// but there are some subtle differences from time to time. For example, +// 'getc' may be defined as macro in stdio.h, and a function in cstdio +#ifdef __cplusplus +#include +#include +#include +#include +#include +#include +#include +#include +#else #include #include -#include #include #include #include #include #include +#include +#endif +#include +#include #include -#include #include #include #include diff --git a/infer/src/clang/cLocation.ml b/infer/src/clang/cLocation.ml index fbabc96ae..ab1488bcb 100644 --- a/infer/src/clang/cLocation.ml +++ b/infer/src/clang/cLocation.ml @@ -118,13 +118,14 @@ let should_translate (loc_start, loc_end) decl_trans_context = in let file_in_project = map_path_of file_in_project loc_end || map_path_of file_in_project loc_start in + let translate_on_demand = file_in_project || Config.models_mode in let file_in_models = map_path_of DB.file_is_in_cpp_model loc_end || map_path_of DB.file_is_in_cpp_model loc_start in equal_current_source !curr_file || map_file_of equal_current_source loc_end || map_file_of equal_current_source loc_start || file_in_models - || (Config.cxx_experimental && decl_trans_context = `Translation && file_in_project + || (Config.cxx_experimental && decl_trans_context = `Translation && translate_on_demand && not Config.testing_mode) let should_translate_lib source_range decl_trans_context = diff --git a/infer/tests/codetoanalyze/cpp/errors/c_tests/c_bugs.cpp b/infer/tests/codetoanalyze/cpp/errors/c_tests/c_bugs.cpp index 3e5283b09..131e7d01e 100644 --- a/infer/tests/codetoanalyze/cpp/errors/c_tests/c_bugs.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/c_tests/c_bugs.cpp @@ -41,3 +41,21 @@ void memcpy_spec_is_found() { memcpy(0, &x, sizeof(int)); int p = 1 / 0; // infer won't reach it when memcpy spec is found } + +// taken from getc.c e2e test +void crash_getc() { + FILE* f; + int i; + f = fopen("this_file_doesnt_exist", "r"); + i = getc(f); + fclose(f); +} + +// taken from getc.c e2e test +void crash_fgetc() { + FILE* f; + int i; + f = fopen("this_file_doesnt_exist", "r"); + i = fgetc(f); + fclose(f); +} diff --git a/infer/tests/endtoend/cpp/CBugsTest.java b/infer/tests/endtoend/cpp/CBugsTest.java index 3cdc61e87..ee585341f 100644 --- a/infer/tests/endtoend/cpp/CBugsTest.java +++ b/infer/tests/endtoend/cpp/CBugsTest.java @@ -112,4 +112,23 @@ public class CBugsTest { doesNotContain(DIVIDE_BY_ZERO, FILE, "memcpy_spec_is_found")); } + @Test + public void whenInferRunsOnGetcCrashThenNullDereferenceIsFound() + throws InterruptedException, IOException, InferException { + InferResults inferResults = InferRunner.runInferCPP(inferCmd); + assertThat( + "Not checking malloc result should report null dereference", + inferResults, + contains(NULL_DEREFERENCE, FILE, "crash_getc")); + } + + @Test + public void whenInferRunsOnFgetcCrashThenNullDereferenceIsFound() + throws InterruptedException, IOException, InferException { + InferResults inferResults = InferRunner.runInferCPP(inferCmd); + assertThat( + "Not checking malloc result should report null dereference", + inferResults, + contains(NULL_DEREFERENCE, FILE, "crash_fgetc")); + } }