diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 994b88ac7..a13b06471 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -326,14 +326,6 @@ OPTIONS --uninit-only Activates: Enable --uninit and disable all other checkers (Conversely: --no-uninit-only) -BIABDUCTION CHECKER OPTIONS - --biabduction-fallback-model-alloc-pattern string - Regex of methods that should be modelled as allocs if definition - is missing - - --biabduction-fallback-model-free-pattern string - Regex of methods that should be modelled as free if definition is - missing BUCK OPTIONS --merge Activates: Merge the captured results directories specified in the diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index aeb9c22b5..8eae764f0 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -114,14 +114,6 @@ OPTIONS using the checkers framework (Conversely: --biabduction) See also infer-analyze(1). - --biabduction-fallback-model-alloc-pattern string - Regex of methods that should be modelled as allocs if definition - is missing See also infer-analyze(1). - - --biabduction-fallback-model-free-pattern string - Regex of methods that should be modelled as free if definition is - missing See also infer-analyze(1). - --biabduction-only Activates: Enable --biabduction and disable all other checkers (Conversely: --no-biabduction-only) See also infer-analyze(1). @@ -1163,12 +1155,6 @@ INTERNAL OPTIONS /my/source/File.java with project root /my/root into ../source/File.java - --biabduction-fallback-model-alloc-pattern-reset - Cancel the effect of --biabduction-fallback-model-alloc-pattern. - - --biabduction-fallback-model-free-pattern-reset - Cancel the effect of --biabduction-fallback-model-free-pattern. - --biabduction-models-mode Activates: Mode for analyzing the biabduction models (Conversely: --no-biabduction-models-mode) diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index a328dd401..68185e241 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -114,14 +114,6 @@ OPTIONS using the checkers framework (Conversely: --biabduction) See also infer-analyze(1). - --biabduction-fallback-model-alloc-pattern string - Regex of methods that should be modelled as allocs if definition - is missing See also infer-analyze(1). - - --biabduction-fallback-model-free-pattern string - Regex of methods that should be modelled as free if definition is - missing See also infer-analyze(1). - --biabduction-only Activates: Enable --biabduction and disable all other checkers (Conversely: --no-biabduction-only) See also infer-analyze(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 396bc7393..51112db27 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -129,8 +129,6 @@ let ivar_attributes = "ivar_attributes" let java_lambda_marker_infix = "$Lambda$" -let manual_biabduction = "BIABDUCTION CHECKER OPTIONS" - let manual_buck = "BUCK OPTIONS" let manual_buffer_overrun = "BUFFER OVERRUN OPTIONS" @@ -645,18 +643,6 @@ and array_level = |} -and biabduction_model_alloc_pattern = - CLOpt.mk_string_opt ~long:"biabduction-fallback-model-alloc-pattern" - ~in_help:InferCommand.[(Analyze, manual_biabduction)] - "Regex of methods that should be modelled as allocs if definition is missing" - - -and biabduction_model_free_pattern = - CLOpt.mk_string_opt ~long:"biabduction-fallback-model-free-pattern" - ~in_help:InferCommand.[(Analyze, manual_biabduction)] - "Regex of methods that should be modelled as free if definition is missing" - - and bootclasspath = CLOpt.mk_string_opt ~long:"bootclasspath" ~in_help:InferCommand.[(Capture, manual_java)] @@ -2536,10 +2522,6 @@ and append_buck_flavors = !append_buck_flavors and array_level = !array_level -and biabduction_model_alloc_pattern = Option.map ~f:Str.regexp !biabduction_model_alloc_pattern - -and biabduction_model_free_pattern = Option.map ~f:Str.regexp !biabduction_model_free_pattern - and biabduction_models_mode = !biabduction_models_mode and bootclasspath = !bootclasspath diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 56a1db59d..e4c652bf5 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -172,10 +172,6 @@ val anon_args : string list val array_level : int -val biabduction_model_alloc_pattern : Str.regexp option - -val biabduction_model_free_pattern : Str.regexp option - val biabduction_models_mode : bool val bo_debug : int diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 4c0af61d7..66219c658 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1398,19 +1398,6 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t let ret_type = attrs.ProcAttributes.ret_type in let model_as_malloc ret_type resolved_pname = Objc_models.is_malloc_model ret_type resolved_pname - || - match Config.biabduction_model_alloc_pattern with - | Some pat -> - Str.string_match pat (Procname.to_string resolved_pname) 0 - | None -> - false - in - let model_as_free resolved_pname = - match Config.biabduction_model_free_pattern with - | Some pat -> - Str.string_match pat (Procname.to_string resolved_pname) 0 - | None -> - false in match attrs.ProcAttributes.objc_accessor with | Some objc_accessor -> @@ -1422,10 +1409,6 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t (* If it's an alloc model, call alloc rather than skipping *) sym_exec_alloc_model exe_env resolved_pname ret_type tenv ret_id_typ current_summary loc prop path - | None when model_as_free resolved_pname -> - (* If it's an free model, call free rather than skipping *) - sym_exec_free_model exe_env ret_id_typ n_actual_params tenv - current_summary loc prop path | _ -> let is_objc_instance_method = ClangMethodKind.equal attrs.ProcAttributes.clang_method_kind @@ -1825,13 +1808,6 @@ and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ summary loc prop instrs exe_env tenv summary (Instrs.singleton alloc_instr) [(prop, path)] -and sym_exec_free_model exe_env ret_id_typ args tenv summary loc prop path : Builtin.ret_typ = - let free_fun = Exp.Const (Const.Cfun BuiltinDecl.free) in - let free_instr = Sil.Call (ret_id_typ, free_fun, args, loc, CallFlags.default) in - L.d_strln "No spec found, method is modelled as free, executing free... " ; - instrs exe_env tenv summary (Instrs.singleton free_instr) [(prop, path)] - - (** Perform symbolic execution for a function call *) and proc_call exe_env callee_summary {Builtin.summary; tenv; prop_= pre; path; ret_id_typ; args= actual_pars; loc} = diff --git a/infer/tests/codetoanalyze/objc/errors/Makefile b/infer/tests/codetoanalyze/objc/errors/Makefile index 85c68637b..c2c46684e 100644 --- a/infer/tests/codetoanalyze/objc/errors/Makefile +++ b/infer/tests/codetoanalyze/objc/errors/Makefile @@ -9,8 +9,7 @@ CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS) CLEAN_EXTRA = infer-out-arc infer-out-all infer-out-all infer-out-arc \ issues.exp.test.all issues.exp.test.arc issues.exp.test.default -INFER_OPTIONS = --biabduction-only --dump-duplicate-symbols --debug-exceptions --project-root $(TESTS_DIR) \ - --biabduction-fallback-model-alloc-pattern AB[IF].*Create.* --biabduction-fallback-model-free-pattern ABFRelease +INFER_OPTIONS = --biabduction-only --dump-duplicate-symbols --debug-exceptions --project-root $(TESTS_DIR) INFERPRINT_OPTIONS = --issues-tests SOURCES_DEFAULT = \ @@ -22,7 +21,6 @@ SOURCES_DEFAULT = \ memory_leaks_benchmark/CoreVideoExample.m \ memory_leaks_benchmark/RetainCycleLength3.m \ memory_leaks_benchmark/ReleasedInBlock.m \ - memory_leaks_benchmark/BAPatLeak.m \ npe/dynamic_dispatch.m \ npe/Fraction.m \ npe/NPD_core_foundation.m \ diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 0529b93b2..4c4cc3b08 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/infer/tests/codetoanalyze/objc/errors/issues.exp @@ -71,7 +71,6 @@ codetoanalyze/objc/errors/subtyping/KindOfClassExample.m, shouldThrowDivideByZer codetoanalyze/objc/errors/subtyping/KindOfClassExample.m, shouldThrowDivideByZero2, 2, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure shouldThrowDivideByZero2(),start of procedure init,return from a call to Base::init,start of procedure returnsZero2(),Taking false branch,return from a call to returnsZero2] codetoanalyze/objc/errors/subtyping/KindOfClassExample.m, shouldThrowDivideByZero3, 3, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure shouldThrowDivideByZero3(),start of procedure init,return from a call to Derived::init,Taking true branch] codetoanalyze/objc/errors/variadic_methods/premature_nil_termination.m, PrematureNilTermA::nilInArrayWithObjects, 5, PREMATURE_NIL_TERMINATION_ARGUMENT, B1, ERROR, [start of procedure nilInArrayWithObjects] -codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m, A::someMethod_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [start of procedure someMethod_bad] codetoanalyze/objc/errors/memory_leaks_benchmark/CoreVideoExample.m, CoreVideoExample::cvpixelbuffer_not_released_leak, 1, MEMORY_LEAK, no_bucket, ERROR, [start of procedure cvpixelbuffer_not_released_leak] codetoanalyze/objc/errors/memory_leaks_benchmark/NSData_models_tests.m, NSData_models_tests::macForIV:, 2, MEMORY_LEAK, no_bucket, ERROR, [start of procedure macForIV:] codetoanalyze/objc/errors/memory_leaks_benchmark/NSString_models_tests.m, StringInitA::hexStringValue, 11, MEMORY_LEAK, no_bucket, ERROR, [start of procedure hexStringValue,Skipping CFStringCreateWithBytesNoCopy(): method has no implementation,Taking false branch] diff --git a/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m b/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m deleted file mode 100644 index 3287e3854..000000000 --- a/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/BAPatLeak.m +++ /dev/null @@ -1,33 +0,0 @@ -/* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ -#include -#include - -typedef struct ABFDataRef { -} ABFDataRef; - -// if impl is there --biabduction-fallback-model-alloc-pattern wont catch it -ABFDataRef* ABFDataCreate(size_t size); -void ABRelease(ABFDataRef*); - -@interface A : NSObject -@end - -@implementation A - -- (void)someMethod_bad { - ABFDataRef* someData = ABFDataCreate(4); - // this allocates a new ABFData structure -} - -- (void)someMethod_ok { - ABFDataRef* someData = ABFDataCreate(4); - // this allocates a new ABFData structure - ABFRelease(someData); -} - -@end