diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index 9ebafef84..617e650b9 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -140,7 +140,7 @@ let execute___print_value { Builtin.tenv; pdesc; prop_; path; args; } let is_undefined_opt tenv prop n_lexp = let is_undef = Option.is_some (Attribute.get_undef tenv prop n_lexp) in - is_undef && (Config.angelic_execution || Config.optimistic_cast) + is_undef && Config.angelic_execution (** Creates an object in the heap with a given type, when the object is not known to be null or when it doesn't appear already in the heap. *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index eb3feb757..05616e2b2 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -940,10 +940,6 @@ and only_footprint = CLOpt.mk_bool ~deprecated:["only_footprint"] ~long:"only-footprint" "Skip the re-execution phase" -and optimistic_cast = - CLOpt.mk_bool ~deprecated:["optimistic_cast"] ~long:"optimistic-cast" - "Allow cast of undefined values" - and out_file = CLOpt.mk_path ~deprecated:["out_file"] ~long:"out-file" ~default:"" ~meta:"file" "Specify the file for the non-error logs of the analyzer" @@ -1451,7 +1447,6 @@ and nelseg = !nelseg and no_translate_libs = not !headers and objc_memory_model_on = !objc_memory_model and only_footprint = !only_footprint -and optimistic_cast = !optimistic_cast and out_file_cmdline = !out_file and patterns_never_returning_null = match patterns_never_returning_null with (k,r) -> (k,!r) and patterns_skip_translation = match patterns_skip_translation with (k,r) -> (k,!r) diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index c27837724..f6a73470d 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -217,7 +217,6 @@ val nelseg : bool val no_translate_libs : bool val objc_memory_model_on : bool val only_footprint : bool -val optimistic_cast : bool val out_file_cmdline : string val pmd_xml : bool val precondition_stats : bool