Skip to content
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/goblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ let main () =
print_endline (localtime ());
print_endline command;
);
let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_and_merge) in
let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
if get_bool "server.enabled" then (
let file =
if get_bool "server.reparse" then
Expand Down
15 changes: 10 additions & 5 deletions src/maingoblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -332,8 +332,8 @@ let preprocess_files () =
);
preprocessed

(** Possibly merge all postprocessed files *)
let merge_preprocessed preprocessed =
(** Parse preprocessed files *)
let parse_preprocessed preprocessed =
(* get the AST *)
if get_bool "dbg.verbose" then print_endline "Parsing files.";

Expand All @@ -358,8 +358,10 @@ let merge_preprocessed preprocessed =

Cilfacade.getAST preprocessed_file
in
let files_AST = List.map (get_ast_and_record_deps) preprocessed 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
Expand All @@ -368,7 +370,7 @@ let merge_preprocessed preprocessed =

(* we use CIL to merge all inputs to ONE file *)
let merged_AST =
match files_AST with
match parsed with
| [one] -> Cilfacade.callConstructors one
| [] ->
prerr_endline "No files to analyze!";
Expand All @@ -383,7 +385,10 @@ let merge_preprocessed preprocessed =
Cilfacade.current_file := merged_AST;
merged_AST

let preprocess_and_merge () = preprocess_files () |> merge_preprocessed
let preprocess_parse_merge () =
preprocess_files ()
|> parse_preprocessed
|> merge_parsed

let do_stats () =
if get_bool "printstats" then (
Expand Down
16 changes: 15 additions & 1 deletion src/util/server.ml
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ let start file =
let reparse (s: t) =
if GobConfig.get_bool "server.reparse" then (
GoblintDir.init ();
let file = Fun.protect ~finally:GoblintDir.finalize Maingoblint.preprocess_and_merge in
let file = Fun.protect ~finally:GoblintDir.finalize Maingoblint.preprocess_parse_merge in
begin match s.file with
| None ->
let max_ids = MaxIdUtil.get_file_max_ids file in
Expand Down Expand Up @@ -232,6 +232,20 @@ let () =
let process () _ = Preprocessor.dependencies_to_yojson ()
end);

register (module struct
let name = "pre_files"
type params = unit [@@deriving of_yojson]
type response = Yojson.Safe.t [@@deriving to_yojson]
let process () s =
if GobConfig.get_bool "server.reparse" then (
GoblintDir.init ();
Fun.protect ~finally:GoblintDir.finalize (fun () ->
ignore Maingoblint.(preprocess_files () |> parse_preprocessed)
)
);
Preprocessor.dependencies_to_yojson ()
end);

register (module struct
let name = "exp_eval"
type params = ExpressionEvaluation.query [@@deriving of_yojson]
Expand Down