diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 927624fab..f48597e60 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -236,6 +236,9 @@ OPTIONS be used on pathologically large procedures to prevent too-big states from being produced. + --pulse-model-abort +string + Methods that should be modelled as abort in Pulse + --pulse-model-alloc-pattern string Regex of methods that should be modelled as allocs in Pulse diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 3970b6687..d448a13f8 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -901,6 +901,9 @@ OPTIONS be used on pathologically large procedures to prevent too-big states from being produced. See also infer-analyze(1). + --pulse-model-abort +string + Methods that should be modelled as abort in Pulse See also infer-analyze(1). + --pulse-model-alloc-pattern string Regex of methods that should be modelled as allocs in Pulse See also infer-analyze(1). @@ -1687,6 +1690,9 @@ INTERNAL OPTIONS --pulse-max-disjuncts int Under-approximate after int disjunctions in the domain + --pulse-model-abort-reset + Set --pulse-model-abort to the empty list. + --pulse-model-alloc-pattern-reset Cancel the effect of --pulse-model-alloc-pattern. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 2d146e91e..ae3d3dc9e 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -901,6 +901,9 @@ OPTIONS be used on pathologically large procedures to prevent too-big states from being produced. See also infer-analyze(1). + --pulse-model-abort +string + Methods that should be modelled as abort in Pulse See also infer-analyze(1). + --pulse-model-alloc-pattern string Regex of methods that should be modelled as allocs in Pulse See also infer-analyze(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 93800f45a..c3fb31220 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1841,6 +1841,12 @@ and pulse_max_disjuncts = "Under-approximate after $(i,int) disjunctions in the domain" +and pulse_model_abort = + CLOpt.mk_string_list ~long:"pulse-model-abort" + ~in_help:InferCommand.[(Analyze, manual_generic)] + "Methods that should be modelled as abort in Pulse" + + and pulse_model_alloc_pattern = CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern" ~in_help:InferCommand.[(Analyze, manual_generic)] @@ -2981,6 +2987,8 @@ and pulse_intraprocedural_only = !pulse_intraprocedural_only and pulse_max_disjuncts = !pulse_max_disjuncts +and pulse_model_abort = !pulse_model_abort + and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_pattern and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 8a50db76c..0179904c0 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -461,6 +461,8 @@ val pulse_intraprocedural_only : bool val pulse_max_disjuncts : int +val pulse_model_abort : string list + val pulse_model_alloc_pattern : Str.regexp option val pulse_model_release_pattern : Str.regexp option diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index f010afff7..44f66030b 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -713,8 +713,19 @@ module ProcNameDispatcher = struct in transfer_ownership_namespace_matchers @ transfer_ownership_name_matchers in + let abort_matchers = + let cpp_separator_regex = Str.regexp_string "::" in + List.filter_map + ~f:(fun m -> + match Str.split cpp_separator_regex m with + | [] -> + None + | first :: rest -> + Some (List.fold rest ~f:( &:: ) ~init:(-first) &--> Misc.early_exit) ) + Config.pulse_model_abort + in make_dispatcher - ( transfer_ownership_matchers + ( transfer_ownership_matchers @ abort_matchers @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete diff --git a/infer/tests/codetoanalyze/cpp/pulse/Makefile b/infer/tests/codetoanalyze/cpp/pulse/Makefile index a479a7f50..5bc5ca8ae 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/Makefile +++ b/infer/tests/codetoanalyze/cpp/pulse/Makefile @@ -7,7 +7,8 @@ TESTS_DIR = ../../.. # see explanations in cpp/biabduction/Makefile for the custom isystem CLANG_OPTIONS = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c -INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) +INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ +--pulse-model-abort "ns1::ns2::fun_abort" INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.cpp) diff --git a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp index 684647d0d..bb628a846 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp @@ -6,6 +6,8 @@ */ #include +#include +#include void assign_zero_ok() { int x[2]; @@ -90,3 +92,33 @@ void std_false_type_deref_bad() { *x = 42; } } + +std::atomic global_var{true}; + +namespace ns1 { +namespace ns2 { +void fun_abort(bool b) { + bool abort = true; + if (b) { + abort = global_var.load(); + } else { + abort = true; + } + if (abort) { + std::abort(); + } +} +} // namespace ns2 +} // namespace ns1 + +X* getX(bool b) { + if (b) { + return new X(); + } else { + ns1::ns2::fun_abort(true); + } + + return nullptr; +} + +void call_modeled_abort_ok() { getX(false)->foo(); }