diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 6a177cf29..4727194d2 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1737,12 +1737,6 @@ INTERNAL OPTIONS --sources-reset Set --sources to the empty list. - --specs-library,-L +dir|jar - Search for .spec files in given directory or jar file - - --specs-library-reset - Set --specs-library to the empty list. - --sqlite-vfs string VFS for SQLite diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index cd2ac807d..243170464 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -157,11 +157,6 @@ module OnDisk = struct [Config.specs_dir_name; specs_filename pname] - (** paths to the .specs file for the given procedure in the current spec libraries *) - let specs_library_filename specs_dir pname = - DB.filename_from_string (Filename.concat specs_dir (specs_filename pname)) - - (** paths to the .specs file for the given procedure in the models folder *) let specs_models_filename pname = DB.filename_from_string (Filename.concat Config.biabduction_models_dir (specs_filename pname)) @@ -186,14 +181,6 @@ module OnDisk = struct (** Load procedure summary for the given procedure name and update spec table *) let load_summary_to_spec_table = - let rec or_load_summary_libs specs_dirs proc_name summ_opt = - match (summ_opt, specs_dirs) with - | Some _, _ | _, [] -> - summ_opt - | None, specs_dir :: specs_dirs -> - load_from_file (specs_library_filename specs_dir proc_name) - |> or_load_summary_libs specs_dirs proc_name - in let load_summary_ziplibs zip_specs_filename = let zip_specs_path = Filename.concat Config.specs_dir_name zip_specs_filename in ZipLib.load summary_serializer zip_specs_path @@ -206,7 +193,6 @@ module OnDisk = struct load_from_file (specs_filename_of_procname proc_name) |> or_from load_from_file specs_models_filename proc_name |> or_from load_summary_ziplibs specs_filename proc_name - |> or_load_summary_libs Config.specs_library proc_name in Option.iter ~f:(add proc_name) summ_opt ; summ_opt diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 014ef87e1..00bc272f1 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -7,7 +7,6 @@ *) open! IStd -open PolyVariantEqual (** Configuration values: either constant, determined at compile time, or set at startup time by system calls, environment variables, or command line options *) @@ -2239,35 +2238,6 @@ and starvation_whole_program = "Run whole-program starvation analysis" -and specs_library = - let specs_library = - CLOpt.mk_path_list ~deprecated:["lib"] ~long:"specs-library" ~short:'L' ~meta:"dir|jar" - "Search for .spec files in given directory or jar file" - in - let (_ : string ref) = - (* Given a filename with a list of paths, convert it into a list of string iff they are - absolute *) - let read_specs_dir_list_file fname = - match Utils.read_file (resolve fname) with - | Ok pathlist -> - pathlist - | Error error -> - L.(die UserError) "cannot read file '%s' from cwd '%s': %s" fname (Sys.getcwd ()) error - in - (* Add the newline-separated directories listed in to the list of directories to be - searched for .spec files *) - CLOpt.mk_path - ~deprecated:["specs-dir-list-file"; "-specs-dir-list-file"] - ~long:"specs-library-index" ~default:"" - ~f:(fun file -> - specs_library := read_specs_dir_list_file file @ !specs_library ; - "" ) - ~in_help:InferCommand.[(Analyze, manual_generic)] - ~meta:"file" "" - in - specs_library - - and sqlite_cache_size = CLOpt.mk_int ~long:"sqlite-cache-size" ~default:2000 ~in_help: @@ -2518,18 +2488,6 @@ let javac_classes_out = "" -and _ = - CLOpt.mk_string_opt ~parse_mode:CLOpt.Javac ~deprecated:["classpath"; "cp"] ~long:"" - ~f:(fun classpath -> - if !buck then ( - let paths = String.split classpath ~on:':' in - let files = List.filter paths ~f:(fun path -> Sys.is_file path = `Yes) in - CLOpt.extend_env_args (List.concat_map files ~f:(fun file -> ["--specs-library"; file])) ; - specs_library := List.rev_append files !specs_library ) ; - classpath ) - "" - - and () = CLOpt.mk_set ~parse_mode:CLOpt.Javac version ~deprecated:["version"] ~long:"" `Javac "" and (_ : bool ref) = @@ -3341,8 +3299,6 @@ let clang_frontend_action_string = information found in the abstract state *) let dynamic_dispatch = biabduction -let specs_library = !specs_library - let quandaryBO_filtered_issues = if quandaryBO then IssueType. diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 90e5c0e74..67d0c993a 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -646,8 +646,6 @@ val source_files_type_environment : bool val source_preview : bool -val specs_library : string list - val sqlite_cache_size : int val sqlite_page_size : int diff --git a/infer/src/base/ZipLib.ml b/infer/src/base/ZipLib.ml index 37ab5152b..ed297233f 100644 --- a/infer/src/base/ZipLib.ml +++ b/infer/src/base/ZipLib.ml @@ -32,35 +32,17 @@ let zip_libraries = (* delay until load is called, to avoid stating/opening files at init time *) lazy (let mk_zip_lib zip_filename = {zip_filename; zip_channel= lazy (Zip.open_in zip_filename)} in - let zip_libs = - let load_zip fname = - if Filename.check_suffix fname ".jar" then - (* fname is a zip of specs *) - Some (mk_zip_lib fname) - else (* fname is a dir of specs *) - None - in - (* Order matters: jar files should appear in the order in which they should be searched for - specs files. [Config.specs_library] is in reverse order of appearance on the command - line. *) - List.rev_filter_map Config.specs_library ~f:load_zip - in if Config.biabduction && (not Config.biabduction_models_mode) && Sys.file_exists Config.biabduction_models_jar = `Yes - then mk_zip_lib Config.biabduction_models_jar :: zip_libs - else zip_libs ) + then Some (mk_zip_lib Config.biabduction_models_jar) + else None ) -(** Search path in the list of zip libraries and use a cache directory to save already deserialized - data *) let load serializer path = - let rec loop = function - | [] -> - None - | zip_library :: other_libraries -> - let opt = load_data serializer path zip_library in - if Option.is_some opt then opt else loop other_libraries - in - loop (Lazy.force zip_libraries) + (* NOTE: This and [zib_libraries] used to also work with a list of where to find "zip libraries" + but now this only handles at most one such library: the biabduction models. There's a chance + that this code looks weirder than it should as a result. *) + Option.bind (Lazy.force zip_libraries) ~f:(fun zip_library -> + load_data serializer path zip_library )