Skip to content

Commit 712e5dd

Browse files
authored
Merge pull request #740 from goblint/issue-739
Add server command `pre_files`
2 parents 4ec572b + 8fc9b36 commit 712e5dd

File tree

3 files changed

+26
-7
lines changed

3 files changed

+26
-7
lines changed

src/goblint.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ let main () =
2323
print_endline (localtime ());
2424
print_endline Goblintutil.command_line;
2525
);
26-
let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_and_merge) in
26+
let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
2727
if get_bool "server.enabled" then (
2828
let file =
2929
if get_bool "server.reparse" then

src/maingoblint.ml

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -313,8 +313,8 @@ let preprocess_files () =
313313
);
314314
preprocessed
315315

316-
(** Possibly merge all postprocessed files *)
317-
let merge_preprocessed preprocessed =
316+
(** Parse preprocessed files *)
317+
let parse_preprocessed preprocessed =
318318
(* get the AST *)
319319
if get_bool "dbg.verbose" then print_endline "Parsing files.";
320320

@@ -339,8 +339,10 @@ let merge_preprocessed preprocessed =
339339

340340
Cilfacade.getAST preprocessed_file
341341
in
342-
let files_AST = List.map (get_ast_and_record_deps) preprocessed in
342+
List.map get_ast_and_record_deps preprocessed
343343

344+
(** Merge parsed files *)
345+
let merge_parsed parsed =
344346
let cilout =
345347
if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout")
346348
in
@@ -349,7 +351,7 @@ let merge_preprocessed preprocessed =
349351

350352
(* we use CIL to merge all inputs to ONE file *)
351353
let merged_AST =
352-
match files_AST with
354+
match parsed with
353355
| [one] -> Cilfacade.callConstructors one
354356
| [] ->
355357
prerr_endline "No files to analyze!";
@@ -364,7 +366,10 @@ let merge_preprocessed preprocessed =
364366
Cilfacade.current_file := merged_AST;
365367
merged_AST
366368

367-
let preprocess_and_merge () = preprocess_files () |> merge_preprocessed
369+
let preprocess_parse_merge () =
370+
preprocess_files ()
371+
|> parse_preprocessed
372+
|> merge_parsed
368373

369374
let do_stats () =
370375
if get_bool "printstats" then (

src/util/server.ml

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,7 @@ let start file =
141141
let reparse (s: t) =
142142
if GobConfig.get_bool "server.reparse" then (
143143
GoblintDir.init ();
144-
let file = Fun.protect ~finally:GoblintDir.finalize Maingoblint.preprocess_and_merge in
144+
let file = Fun.protect ~finally:GoblintDir.finalize Maingoblint.preprocess_parse_merge in
145145
begin match s.file with
146146
| None ->
147147
let max_ids = MaxIdUtil.get_file_max_ids file in
@@ -257,6 +257,20 @@ let () =
257257
let process () _ = Preprocessor.dependencies_to_yojson ()
258258
end);
259259

260+
register (module struct
261+
let name = "pre_files"
262+
type params = unit [@@deriving of_yojson]
263+
type response = Yojson.Safe.t [@@deriving to_yojson]
264+
let process () s =
265+
if GobConfig.get_bool "server.reparse" then (
266+
GoblintDir.init ();
267+
Fun.protect ~finally:GoblintDir.finalize (fun () ->
268+
ignore Maingoblint.(preprocess_files () |> parse_preprocessed)
269+
)
270+
);
271+
Preprocessor.dependencies_to_yojson ()
272+
end);
273+
260274
register (module struct
261275
let name = "functions"
262276
type params = unit [@@deriving of_yojson]

0 commit comments

Comments
 (0)