package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/src/goblint.incremental/serialize.ml.html
Source file serialize.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
(** Serialization/deserialization of incremental analysis data. *) open Batteries (* TODO: GoblintDir *) let incremental_data_file_name = "analysis.data" let results_dir = "results" type operation = Save | Load (** Returns the name of the directory used for loading/saving incremental data *) let incremental_dirname op = match op with | Load -> GobConfig.get_string "incremental.load-dir" | Save -> GobConfig.get_string "incremental.save-dir" let gob_directory op = GobFpath.cwd_append (Fpath.v (incremental_dirname op)) let gob_results_dir op = Fpath.(gob_directory op / results_dir) let server () = GobConfig.get_bool "server.enabled" let marshal obj fileName = let chan = open_out_bin (Fpath.to_string fileName) in Marshal.output chan obj; close_out chan let unmarshal fileName = Logs.debug "Unmarshalling %s... If type of content changed, this will result in a segmentation fault!" (Fpath.to_string fileName); Marshal.input (open_in_bin (Fpath.to_string fileName)) let results_exist () = (* If Goblint did not crash irregularly, the existence of the result directory indicates that there are results *) let r = gob_results_dir Load in let r_str = Fpath.to_string r in Sys.file_exists r_str && Sys.is_directory r_str (** Module to cache the data for incremental analaysis during a run, before it is stored to disk, as well as for the server mode *) module Cache = struct type t = { mutable solver_data: Obj.t option; mutable analysis_data: Obj.t option; mutable version_data: MaxIdUtil.max_ids option; mutable cil_file: GoblintCil.file option; } let data = ref { solver_data = None; analysis_data = None; version_data = None; cil_file = None; } (** GADT that may be used to query data from and pass data to the cache. *) type _ data_query = | SolverData : _ data_query | CilFile : GoblintCil.file data_query | VersionData : MaxIdUtil.max_ids data_query | AnalysisData : _ data_query (** Loads data for incremental runs from the appropriate file *) let load_data () = let p = Fpath.(gob_results_dir Load / incremental_data_file_name) in let loaded_data = unmarshal p in data := loaded_data (** Stores data for future incremental runs at the appropriate file. *) let store_data () = GobSys.mkdir_or_exists (gob_directory Save); let d = gob_results_dir Save in GobSys.mkdir_or_exists d; let p = Fpath.(d / incremental_data_file_name) in marshal !data p (** Update the incremental data in the in-memory cache *) let update_data: type a. a data_query -> a -> unit = fun q d -> match q with | SolverData -> !data.solver_data <- Some (Obj.repr d) | AnalysisData -> !data.analysis_data <- Some (Obj.repr d) | VersionData -> !data.version_data <- Some d | CilFile -> !data.cil_file <- Some d (** Reset some incremental data in the in-memory cache to [None]*) let reset_data : type a. a data_query -> unit = function | SolverData -> !data.solver_data <- None | AnalysisData -> !data.analysis_data <- None | VersionData -> !data.version_data <- None | CilFile -> !data.cil_file <- None (** Get incremental data from the in-memory cache wrapped in an optional. To populate the in-memory cache with data, call [load_data] first. *) let get_opt_data : type a. a data_query -> a option = function | SolverData -> Option.map Obj.obj !data.solver_data | AnalysisData -> Option.map Obj.obj !data.analysis_data | VersionData -> !data.version_data | CilFile -> !data.cil_file (** Get incremental data from the in-memory cache. Same as [get_opt_data], except not yielding an optional and failing when the requested data is not present. *) let get_data : type a. a data_query -> a = fun a -> match get_opt_data a with | Some d -> d | None -> failwith "Requested data is not loaded." end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>