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 ->
("--" ^ 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
)
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 =
let basename = Fpath.rem_ext (Fpath.base fname) in
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
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;
let cppflags = ref (get_string_list "pre.cppflags") in
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
let include_dirs = ref [] in
let include_files = ref [] in
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 get_bool "kernel" then (
let kernel_root = get_string "pre.kernel-root" in
let kernel_roots =
begin if kernel_root <> "" then
[Fpath.v kernel_root]
else
[]
end @ [
Fpath.(exe_dir / "linux-headers");
]
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
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;
include_dirs := !include_dirs @ [
kernel_dir; Fpath.(kernel_dir / "uapi"); Fpath.(kernel_dir / "include" / "generated" / "uapi");
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
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
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
[]
| 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 = 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 =
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, ) = match path_str with
| "<built-in>" | "<command-line>" ->
(path_str, system_header)
| _ ->
let path = Fpath.v path_str in
let dir = (Option.get task_opt).ProcessPool.cwd |? goblint_cwd in
let path' = Fpath.normalize @@ Fpath.append dir path in
let path' = Fpath.rem_prefix goblint_cwd path' |? path' in
Preprocessor.FpathH.modify_def Fpath.Map.empty preprocessed_file (Fpath.Map.add path' system_header) Preprocessor.dependencies;
(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;
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;
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 =
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
Cilfacade.print merged_AST
else (
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);
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
Goblintutil.should_warn := true;
Messages.error ~category:Analyzer "About to crash!";
Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal")));
do_stats ();
print_newline ();
Printexc.raise_with_backtrace e backtrace
in
Stats.time "analysis" (control_analyze merged_AST) funs
)
let do_html_output () =
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 () =
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 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");
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
let diff_and_rename current_file =
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 () =
let open Sys in
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"))