package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.0.1.tbz
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd
doc/src/goblint.lib/maingoblint.ml.html
Source file maingoblint.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 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546
(** This is the main program! *) open Prelude open GobConfig open Printf open Goblintutil open GoblintCil let writeconffile = ref None (** Print version and bail. *) let print_version ch = printf "Goblint version: %s\n" Version.goblint; printf "Cil version: %s\n" Cil.cilVersion; printf "Profile: %s\n" ConfigProfile.profile; exit 0 (** Print helpful messages. *) let print_help ch = fprintf ch "Usage: goblint [options] source-files\nOptions\n"; fprintf ch " -v Prints more status information. \n"; fprintf ch " -o <file> Prints the output to file. \n"; fprintf ch " -I <dir> Add include directory. \n"; fprintf ch " -IK <dir> Add kernel include directory. \n\n"; fprintf ch " --help Prints this text \n"; fprintf ch " --version Print out current version information. \n\n"; fprintf ch " --conf <file> Merge the configuration from the <file>. \n"; fprintf ch " --writeconf <file> Write the effective configuration to <file> \n"; fprintf ch " --set <jpath> <jvalue> Set a configuration variable <jpath> to the specified <jvalue>.\n"; fprintf ch " --sets <jpath> <string> Set a configuration variable <jpath> to the string.\n"; fprintf ch " --enable <jpath> Set a configuration variable <jpath> to true. \n"; fprintf ch " --disable <jpath> Set a configuration variable <jpath> to false. \n\n"; fprintf ch " --print_options Print out commonly used configuration variables.\n"; fprintf ch " --print_all_options Print out all configuration variables. \n"; fprintf ch "\n"; fprintf ch "A <jvalue> is a string from the JSON language where single-quotes (')"; fprintf ch " are used instead of double-quotes (\").\n\n"; fprintf ch "A <jpath> is a path in a json structure. E.g. 'field.another_field[42]';\n"; fprintf ch "in addition to the normal syntax you can use 'field[+]' append to an array.\n\n"; fprintf ch "Some common configurations to start from can be found in conf/examples/*\n"; exit 0 (** [Arg] option specification *) let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy ( let add_string l = let f str = l := str :: !l in Arg_complete.String (f, Arg_complete.empty) in let add_int l = let f str = l := str :: !l in Arg_complete.Int (f, Arg_complete.empty) in let set_trace sys = if Messages.tracing then Tracing.addsystem sys else (prerr_endline "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Exit) in let configure_html () = if (get_string "outfile" = "") then set_string "outfile" "result"; if get_string "exp.g2html_path" = "" then set_string "exp.g2html_path" (Fpath.to_string exe_dir); set_bool "exp.cfgdot" true; set_bool "g2html" true; set_string "result" "fast_xml" in let configure_sarif () = if (get_string "outfile" = "") then set_string "outfile" "goblint.sarif"; set_string "result" "sarif" in let complete_option_value option s = let completions = List.assoc option Options.completions in Arg_complete.strings completions s in let defaults_spec_list = List.map (fun path -> (* allow "--option value" as shorthand for "--set option value" *) ("--" ^ path, Arg_complete.String (set_auto path, complete_option_value path), "") ) Options.paths in let tmp_arg = ref "" in let last_complete_option = ref "" in let complete_option s = last_complete_option := s; Arg_complete.strings Options.paths s in let complete_bool_option s = let cs = complete_option s in let is_bool c = match GobConfig.get_json c with | `Bool _ -> true | _ -> false in List.filter is_bool cs in let complete_last_option_value s = complete_option_value !last_complete_option s in [ "-o" , Arg_complete.String (set_string "outfile", Arg_complete.empty), "" ; "-v" , Arg_complete.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "printstats" true), "" ; "-j" , Arg_complete.Int (set_int "jobs", Arg_complete.empty), "" ; "-I" , Arg_complete.String (set_string "pre.includes[+]", Arg_complete.empty), "" ; "-IK" , Arg_complete.String (set_string "pre.kernel_includes[+]", Arg_complete.empty), "" ; "--set" , Arg_complete.Tuple [Arg_complete.Set_string (tmp_arg, complete_option); Arg_complete.String ((fun x -> set_auto !tmp_arg x), complete_last_option_value)], "" ; "--sets" , Arg_complete.Tuple [Arg_complete.Set_string (tmp_arg, complete_option); Arg_complete.String ((fun x -> prerr_endline "--sets is deprecated, use --set instead."; set_string !tmp_arg x), complete_last_option_value)], "" ; "--enable" , Arg_complete.String ((fun x -> set_bool x true), complete_bool_option), "" ; "--disable" , Arg_complete.String ((fun x -> set_bool x false), complete_bool_option), "" ; "--conf" , Arg_complete.String ((fun fn -> merge_file (Fpath.v fn)), Arg_complete.empty), "" ; "--writeconf" , Arg_complete.String ((fun fn -> writeconffile := Some (Fpath.v fn)), Arg_complete.empty), "" ; "--version" , Arg_complete.Unit print_version, "" ; "--print_options" , Arg_complete.Unit (fun () -> Options.print_options (); exit 0), "" ; "--print_all_options" , Arg_complete.Unit (fun () -> Options.print_all_options (); exit 0), "" ; "--trace" , Arg_complete.String (set_trace, Arg_complete.empty), "" ; "--tracevars" , add_string Tracing.tracevars, "" ; "--tracelocs" , add_int Tracing.tracelocs, "" ; "--help" , Arg_complete.Unit (fun _ -> print_help stdout),"" ; "--html" , Arg_complete.Unit (fun _ -> configure_html ()),"" ; "--sarif" , Arg_complete.Unit (fun _ -> configure_sarif ()),"" ; "--compare_runs" , Arg_complete.Tuple [Arg_complete.Set_string (tmp_arg, Arg_complete.empty); Arg_complete.String ((fun x -> set_auto "compare_runs" (sprintf "['%s','%s']" !tmp_arg x)), Arg_complete.empty)], "" ; "--complete" , Arg_complete.Rest_all_compat.spec (Lazy.force rest_all_complete), "" ] @ defaults_spec_list (* lowest priority *) ) and rest_all_complete = lazy (Arg_complete.Rest_all_compat.create complete Arg_complete.empty_all) and complete args = Arg_complete.complete_argv args (Lazy.force option_spec_list) Arg_complete.empty |> List.iter print_endline; raise Exit (** Parse arguments. Print help if needed. *) let parse_arguments () = let anon_arg = set_string "files[+]" in let arg_speclist = Arg_complete.arg_speclist (Lazy.force option_spec_list) in Arg.parse arg_speclist anon_arg "Look up options using 'goblint --help'."; Arg_complete.Rest_all_compat.finish (Lazy.force rest_all_complete); begin match !writeconffile with | Some writeconffile -> GobConfig.write_file writeconffile; raise Exit | None -> () end; if get_string_list "files" = [] then ( prerr_endline "No files for Goblint?"; prerr_endline "Try `goblint --help' for more information."; raise Exit ) (** Initialize some globals in other modules. *) let handle_flags () = if get_bool "dbg.verbose" then ( Printexc.record_backtrace true; Errormsg.debugFlag := true; Errormsg.verboseFlag := true ); if get_bool "dbg.debug" then set_bool "warn.debug" true; match get_string "dbg.dump" with | "" -> () | path -> Messages.formatter := Format.formatter_of_out_channel (Legacy.open_out (Legacy.Filename.concat path "warnings.out")); set_string "outfile" "" let basic_preprocess_counts = Preprocessor.FpathH.create 3 (** Use gcc to preprocess a file. Returns the path to the preprocessed file. *) let basic_preprocess ~all_cppflags fname = (* The actual filename of the preprocessed sourcefile *) let basename = Fpath.rem_ext (Fpath.base fname) in (* generate unique preprocessed filename in case multiple basic files have same basename (from different directories), happens in ddverify *) let count = Preprocessor.FpathH.find_default basic_preprocess_counts basename 0 in let unique_name = if count = 0 then basename else Fpath.add_ext (string_of_int count) basename in Preprocessor.FpathH.replace basic_preprocess_counts basename (count + 1); let nname = Fpath.append (GoblintDir.preprocessed ()) (Fpath.add_ext ".i" unique_name) in (* Preprocess using cpp. *) (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *) let arguments = "--undef" :: "__BLOCKS__" :: all_cppflags @ Fpath.to_string fname :: "-o" :: Fpath.to_string nname :: [] in let command = Filename.quote_command (Preprocessor.get_cpp ()) arguments in if get_bool "dbg.verbose" then print_endline command; (nname, Some {ProcessPool.command; cwd = None}) (** Preprocess all files. Return list of preprocessed files and the temp directory name. *) let preprocess_files () = Preprocessor.FpathH.clear basic_preprocess_counts; Preprocessor.FpathH.clear Preprocessor.dependencies; (* clear for server mode *) (* Preprocessor flags *) let cppflags = ref (get_string_list "pre.cppflags") in (* the base include directory *) let custom_include_dirs = List.map Fpath.v (get_string_list "pre.custom_includes") @ Fpath.(exe_dir / "includes") :: List.map Fpath.v Goblint_sites.includes in if get_bool "dbg.verbose" then ( print_endline "Custom include dirs:"; List.iteri (fun i custom_include_dir -> Format.printf " %d. %a (exists=%B)\n" (i + 1) Fpath.pp custom_include_dir (Sys.file_exists (Fpath.to_string custom_include_dir)) ) custom_include_dirs ); let custom_include_dirs = List.filter (Sys.file_exists % Fpath.to_string) custom_include_dirs in if custom_include_dirs = [] then print_endline "Warning, cannot find goblint's custom include files."; let find_custom_include subpath = List.find_map (fun custom_include_dir -> let path = Fpath.append custom_include_dir subpath in if Sys.file_exists (Fpath.to_string path) then Some path else None ) custom_include_dirs in (* include flags*) let include_dirs = ref [] in let include_files = ref [] in (* fill include flags *) let one_include_f f x = include_dirs := f x :: !include_dirs in get_string_list "pre.includes" |> List.map Fpath.v |> List.iter (one_include_f identity); include_dirs := custom_include_dirs @ !include_dirs; include_files := find_custom_include (Fpath.v "goblint.h") :: !include_files; (* If we analyze a kernel module, some special includes are needed. *) if get_bool "kernel" then ( let kernel_root = get_string "pre.kernel-root" in let kernel_roots = begin if kernel_root <> "" then (* cannot parse empty *) [Fpath.v kernel_root] else [] end @ [ Fpath.(exe_dir / "linux-headers"); (* linux-headers not installed with goblint package *) ] in let kernel_root = try List.find (Sys.file_exists % Fpath.to_string) kernel_roots with Not_found -> prerr_endline "Root directory for kernel include files not found!"; raise Exit in let kernel_dir = Fpath.(kernel_root / "include") in let arch_dir = Fpath.(kernel_root / "arch" / "x86" / "include") in (* TODO add arm64: https://github.com/goblint/analyzer/issues/312 *) get_string_list "pre.kernel_includes" |> List.map Fpath.v |> List.iter (Fpath.append kernel_root |> one_include_f); let preconf = find_custom_include Fpath.(v "linux" / "goblint_preconf.h") in let autoconf = Fpath.(kernel_dir / "linux" / "kconfig.h") in cppflags := "-D__KERNEL__" :: "-U__i386__" :: "-D__x86_64__" :: !cppflags; include_files := preconf :: autoconf :: !include_files; (* These are not just random permutations of directories, but based on USERINCLUDE from the * Linux kernel Makefile (in the root directory of the kernel distribution). *) include_dirs := !include_dirs @ [ kernel_dir; Fpath.(kernel_dir / "uapi"); Fpath.(kernel_dir / "include" / "generated" / "uapi"); (* TODO: duplicate include with kernel_dir is bug? *) arch_dir; Fpath.(arch_dir / "generated"); Fpath.(arch_dir / "uapi"); Fpath.(arch_dir / "generated" / "uapi"); ] ); let include_args = List.concat_map (fun include_dir -> ["-I"; Fpath.to_string include_dir]) !include_dirs @ List.concat_map (fun include_file -> ["-include"; Fpath.to_string include_file]) !include_files in let all_cppflags = !cppflags @ include_args in (* preprocess all the files *) if get_bool "dbg.verbose" then print_endline "Preprocessing files."; let rec preprocess_arg_file = function | filename when Fpath.filename filename = "Makefile" -> let comb_file = MakefileUtil.generate_and_combine filename ~all_cppflags in [basic_preprocess ~all_cppflags comb_file] | filename when Fpath.filename filename = CompilationDatabase.basename -> CompilationDatabase.load_and_preprocess ~all_cppflags filename | filename when Sys.is_directory (Fpath.to_string filename) -> let dir_files = Sys.readdir (Fpath.to_string filename) in if Array.mem CompilationDatabase.basename dir_files then (* prefer compilation database to Makefile in case both exist, because compilation database is more robust *) preprocess_arg_file (Fpath.add_seg filename CompilationDatabase.basename) else if Array.mem "Makefile" dir_files then preprocess_arg_file (Fpath.add_seg filename "Makefile") else [] (* don't recurse for anything else *) | filename when Fpath.get_ext filename = ".json" -> Format.eprintf "Unexpected JSON file argument (possibly missing --conf): %a\n" Fpath.pp filename; raise Exit | filename -> [basic_preprocess ~all_cppflags filename] in let extra_files = ref [] in extra_files := find_custom_include (Fpath.v "stdlib.c") :: find_custom_include (Fpath.v "pthread.c") :: !extra_files; if get_bool "ana.sv-comp.functions" then extra_files := find_custom_include (Fpath.v "sv-comp.c") :: !extra_files; let preprocessed = List.concat_map preprocess_arg_file (!extra_files @ List.map Fpath.v (get_string_list "files")) in if not (get_bool "pre.exist") then ( let preprocess_tasks = List.filter_map snd preprocessed in let terminated task = function | Unix.WEXITED 0 -> () | process_status -> failwith (GobUnix.string_of_process_status process_status) in ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks ); preprocessed (** Parse preprocessed files *) let parse_preprocessed preprocessed = (* get the AST *) if get_bool "dbg.verbose" then print_endline "Parsing files."; let goblint_cwd = GobFpath.cwd () in let get_ast_and_record_deps (preprocessed_file, task_opt) = let transform_file (path_str, system_header) = match path_str with | "<built-in>" | "<command-line>" -> (path_str, system_header) (* ignore special "paths" *) | _ -> let path = Fpath.v path_str in let dir = (Option.get task_opt).ProcessPool.cwd |? goblint_cwd in (* relative to compilation database directory or goblint's cwd *) let path' = Fpath.normalize @@ Fpath.append dir path in let path' = Fpath.rem_prefix goblint_cwd path' |? path' in (* remove goblint cwd prefix (if has one) for readability *) Preprocessor.FpathH.modify_def Fpath.Map.empty preprocessed_file (Fpath.Map.add path' system_header) Preprocessor.dependencies; (* record dependency *) (Fpath.to_string path', system_header) in let transformLocation ~file ~line = let file' = Option.map transform_file file in Some (file', line) in Errormsg.transformLocation := transformLocation; Cilfacade.getAST preprocessed_file in List.map get_ast_and_record_deps preprocessed (** Merge parsed files *) let merge_parsed parsed = let cilout = if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout") in Errormsg.logChannel := Messages.get_out "cil" cilout; (* we use CIL to merge all inputs to ONE file *) let merged_AST = match parsed with | [one] -> Cilfacade.callConstructors one | [] -> prerr_endline "No files to analyze!"; raise Exit | xs -> Cilfacade.getMergedAST xs |> Cilfacade.callConstructors in Cilfacade.rmTemps merged_AST; (* create the Control Flow Graph from CIL's AST *) Cilfacade.createCFG merged_AST; Cilfacade.current_file := merged_AST; merged_AST let preprocess_parse_merge () = preprocess_files () |> parse_preprocessed |> merge_parsed let do_stats () = if get_bool "printstats" then ( print_newline (); ignore (Pretty.printf "vars = %d evals = %d narrow_reuses = %d\n" !Goblintutil.vars !Goblintutil.evals !Goblintutil.narrow_reuses); print_newline (); Stats.print (Messages.get_out "timing" Legacy.stderr) "Timings:\n"; flush_all () ) let reset_stats () = Goblintutil.vars := 0; Goblintutil.evals := 0; Goblintutil.narrow_reuses := 0; Stats.reset SoftwareTimer (** Perform the analysis over the merged AST. *) let do_analyze change_info merged_AST = (* direct the output to file if requested *) if not (get_bool "g2html" || get_string "outfile" = "") then ( if !Goblintutil.out <> Legacy.stdout then Legacy.close_out !Goblintutil.out; Goblintutil.out := Legacy.open_out (get_string "outfile")); let module L = Printable.Liszt (CilType.Fundec) in if get_bool "justcil" then (* if we only want to print the output created by CIL: *) Cilfacade.print merged_AST else ( (* we first find the functions to analyze: *) if get_bool "dbg.verbose" then print_endline "And now... the Goblin!"; let (stf,exf,otf as funs) = Cilfacade.getFuns merged_AST in if stf@exf@otf = [] then failwith "No suitable function to start from."; if get_bool "dbg.verbose" then ignore (Pretty.printf "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a\n" L.pretty stf L.pretty exf L.pretty otf); (* and here we run the analysis! *) let control_analyze ast funs = if get_bool "dbg.verbose" then ( let aa = String.concat ", " @@ get_string_list "ana.activated" in let at = String.concat ", " @@ get_string_list "trans.activated" in print_endline @@ "Activated analyses: " ^ aa; print_endline @@ "Activated transformations: " ^ at ); try Control.analyze change_info ast funs with e -> let backtrace = Printexc.get_raw_backtrace () in (* capture backtrace immediately, otherwise the following loses it (internal exception usage without raise_notrace?) *) Goblintutil.should_warn := true; (* such that the `about to crash` message gets printed *) Messages.error ~category:Analyzer "About to crash!"; (* trigger Generic.SolverStats...print_stats *) Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal"))); do_stats (); print_newline (); Printexc.raise_with_backtrace e backtrace (* re-raise with captured inner backtrace *) (* Cilfacade.current_file := ast'; *) in Stats.time "analysis" (control_analyze merged_AST) funs ) let do_html_output () = (* TODO: Fpath *) let jar = Filename.concat (get_string "exp.g2html_path") "g2html.jar" in if get_bool "g2html" then ( if Sys.file_exists jar then ( let command = "java -jar "^ jar ^" --result-dir "^ (get_string "outfile")^" "^ !Messages.xml_file_name in try match Unix.system command with | Unix.WEXITED 0 -> () | _ -> eprintf "HTML generation failed! Command: %s\n" command with Unix.Unix_error (e, f, a) -> eprintf "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a ) else eprintf "Warning: jar file %s not found.\n" jar ) let do_gobview () = (* TODO: Fpath *) let create_symlink target link = if not (Sys.file_exists link) then Unix.symlink target link in let gobview = GobConfig.get_bool "gobview" in let goblint_root = Filename.concat (Unix.getcwd ()) (Filename.dirname Sys.argv.(0)) in let dist_dir = Filename.concat goblint_root "_build/default/gobview/dist" in let js_file = Filename.concat dist_dir "main.js" in if gobview then ( if Sys.file_exists js_file then ( let save_run = GobConfig.get_string "save_run" in let run_dir = if save_run <> "" then save_run else "run" in let dist_files = Sys.files_of dist_dir |> Enum.filter (fun n -> n <> "dune") |> List.of_enum in List.iter (fun n -> create_symlink (Filename.concat dist_dir n) (Filename.concat run_dir n) ) dist_files ) else eprintf "Warning: Cannot locate Gobview.\n" ) let eprint_color m = eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr m) let check_arguments () = (* let fail m = let m = "Option failure: " ^ m in eprint_color ("{red}"^m); failwith m in *) (* unused now, but might be useful for future checks here *) let warn m = eprint_color ("{yellow}Option warning: "^m) in if get_bool "allfuns" && not (get_bool "exp.earlyglobs") then (set_bool "exp.earlyglobs" true; warn "allfuns enables exp.earlyglobs.\n"); if not @@ List.mem "escape" @@ get_string_list "ana.activated" then warn "Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!"; if get_bool "ana.base.context.int" && not (get_bool "ana.base.context.non-ptr") then (set_bool "ana.base.context.int" false; warn "ana.base.context.int implicitly disabled by ana.base.context.non-ptr"); (* order matters: non-ptr=false, int=true -> int=false cascades to interval=false with warning *) if get_bool "ana.base.context.interval" && not (get_bool "ana.base.context.int") then (set_bool "ana.base.context.interval" false; warn "ana.base.context.interval implicitly disabled by ana.base.context.int"); if get_bool "incremental.only-rename" then (set_bool "incremental.load" true; warn "incremental.only-rename implicitly activates incremental.load. Previous AST is loaded for diff and rename, but analyis results are not reused."); if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated." let handle_extraspecials () = let funs = get_string_list "exp.extraspecials" in LibraryFunctions.add_lib_funs funs (* Detects changes and renames vids and sids. *) let diff_and_rename current_file = (* Create change info, either from old results, or from scratch if there are no previous results. *) let change_info: Analyses.increment_data = let warn m = eprint_color ("{yellow}Warning: "^m) in if GobConfig.get_bool "incremental.load" && not (Serialize.results_exist ()) then begin warn "incremental.load is activated but no data exists that can be loaded." end; let (changes, restarting, old_file, max_ids) = if Serialize.results_exist () && GobConfig.get_bool "incremental.load" then begin Serialize.Cache.load_data (); let old_file = Serialize.Cache.(get_data CilFile) in let changes = CompareCIL.compareCilFiles old_file current_file in let max_ids = Serialize.Cache.(get_data VersionData) in let max_ids = UpdateCil.update_ids old_file max_ids current_file changes in let restarting = GobConfig.get_string_list "incremental.restart.list" in let restarting, not_found = VarQuery.varqueries_from_names current_file restarting in if not (List.is_empty not_found) then begin List.iter (fun s -> warn @@ "Should restart " ^ s ^ " but no such global could not be found in the CIL-file.") not_found; flush stderr end; (changes, restarting, Some old_file, max_ids) end else begin let max_ids = MaxIdUtil.get_file_max_ids current_file in (CompareCIL.empty_change_info (), [], None, max_ids) end in let solver_data = if Serialize.results_exist () && GobConfig.get_bool "incremental.load" && not (GobConfig.get_bool "incremental.only-rename") then Some Serialize.Cache.(get_data SolverData) else None in if GobConfig.get_bool "incremental.save" then begin Serialize.Cache.(update_data CilFile current_file); Serialize.Cache.(update_data VersionData max_ids); end; let old_data = match old_file, solver_data with | Some cil_file, Some solver_data -> Some ({solver_data}: Analyses.analyzed_data) | _, _ -> None in {server = false; Analyses.changes = changes; restarting; old_data} in change_info let () = (* signal for printing backtrace; other signals in Generic.SolverStats and Timeout *) let open Sys in (* whether interactive interrupt (ctrl-C) terminates the program or raises the Break exception which we use below to print a backtrace. https://ocaml.org/api/Sys.html#VALcatch_break *) catch_break true; set_signal (Goblintutil.signal_of_string (get_string "dbg.backtrace-signal")) (Signal_handle (fun _ -> Printexc.get_callstack 999 |> Printexc.print_raw_backtrace Stdlib.stderr; print_endline "\n...\n")) (* e.g. `pkill -SIGUSR2 goblint`, or `kill`, `htop` *)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>