diff --git a/goblint.opam b/goblint.opam index b235f85adc..99fc9efdfe 100644 --- a/goblint.opam +++ b/goblint.opam @@ -63,7 +63,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! pin-depends: [ - [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#f8c8fe4da12ebe59a7b87851366dfc49b6e4b9ae" ] + [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#908790cb6c85f5ce053a0616bcc6b327758b8966" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] # quoter workaround reverted for release, so no pin needed diff --git a/goblint.opam.locked b/goblint.opam.locked index d3b76bbe39..01762c0300 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -110,7 +110,7 @@ version: "dev" pin-depends: [ [ "goblint-cil.1.8.2" - "git+https://github.com/goblint/cil.git#f8c8fe4da12ebe59a7b87851366dfc49b6e4b9ae" + "git+https://github.com/goblint/cil.git#908790cb6c85f5ce053a0616bcc6b327758b8966" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index bf9cbbcd8e..3a224e0e5b 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -1,7 +1,7 @@ # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project # also remember to generate/adjust goblint.opam.locked! pin-depends: [ - [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#f8c8fe4da12ebe59a7b87851366dfc49b6e4b9ae" ] + [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#908790cb6c85f5ce053a0616bcc6b327758b8966" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] # quoter workaround reverted for release, so no pin needed diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index a1bca72492..562da97b5c 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -268,19 +268,10 @@ struct printf "Writing Sarif to file: %s\n%!" (get_string "outfile"); Yojson.Safe.pretty_to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); | "json-messages" -> - let files = - let module SH = BatHashtbl.Make (Basetype.RawStrings) in - let files = SH.create 100 in - iterGlobals file (function - | GFun (_, loc) - | GVar (_, _, loc) -> - SH.replace files loc.file (Hashtbl.find_option Preprocessor.dependencies loc.file) - | _ -> () (* TODO: add locs from everything else? would also include system headers *) - ); - files |> SH.to_list - in + let files = Hashtbl.to_list Preprocessor.dependencies in + let filter_system = List.filter_map (fun (f,system) -> if system then None else Some f) in let json = `Assoc [ - ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list option]) files)); + ("files", `Assoc (List.map (Tuple2.map2 (fun deps -> [%to_yojson:string list] @@ filter_system deps)) files)); ("messages", Messages.Table.to_yojson ()); ] in diff --git a/src/maingoblint.ml b/src/maingoblint.ml index e664ef1de1..80958a7783 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -159,14 +159,11 @@ let basic_preprocess ~all_cppflags fname = else (* Preprocess using cpp. *) (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *) - let deps_file = Filename.chop_extension nname ^ ".d" in - let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " -MMD -MT " ^ fname ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in + let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in if get_bool "dbg.verbose" then print_endline command; try match Unix.system command with - | Unix.WEXITED 0 -> - Preprocessor.parse_makefile_deps deps_file; - nname + | Unix.WEXITED 0 -> nname | _ -> eprintf "Goblint: Preprocessing failed."; raise Exit with Unix.Unix_error (e, f, a) -> eprintf "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a; raise Exit @@ -291,7 +288,13 @@ let preprocess_files () = let merge_preprocessed cpp_file_names = (* get the AST *) if get_bool "dbg.verbose" then print_endline "Parsing files."; - let files_AST = List.map Cilfacade.getAST cpp_file_names in + let get_ast_and_record_deps f = + let file = Cilfacade.getAST f in + (* Drop and from dependencies *) + Hashtbl.add Preprocessor.dependencies f @@ List.filter (fun (n,_) -> n <> "" && n <> "") file.files; + file + in + let files_AST = List.map (get_ast_and_record_deps) cpp_file_names in let cilout = if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout") diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index 54a46e2bf8..d93fb0bf4e 100644 --- a/src/util/compilationDatabase.ml +++ b/src/util/compilationDatabase.ml @@ -55,12 +55,11 @@ let load_and_preprocess ~all_cppflags filename = else let preprocessed_file = Filename.concat preprocessed_dir (Filename.chop_extension (GobFilename.chop_common_prefix database_dir file) ^ ".i") in GobSys.mkdir_parents preprocessed_file; - let deps_file = Filename.chop_extension preprocessed_file ^ ".d" in let preprocess_command = match obj.command, obj.arguments with | Some command, None -> (* TODO: extract o_file *) let command = reroot command in - let preprocess_command = Str.replace_first command_program_regexp ("\\1 " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " -E -MMD -MT " ^ file) command in + let preprocess_command = Str.replace_first command_program_regexp ("\\1 " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " -E") command in let preprocess_command = Str.replace_first command_o_regexp ("-o " ^ preprocessed_file) preprocess_command in if preprocess_command = command then (* easier way to check if match was found (and replaced) *) failwith "CompilationDatabase.preprocess: no -o argument found for " ^ file @@ -72,7 +71,7 @@ let load_and_preprocess ~all_cppflags filename = | (o_i, _) -> begin match List.split_at o_i arguments with | (arguments_program :: arguments_init, _ :: o_file :: arguments_tl) -> - let preprocess_arguments = all_cppflags @ "-E" :: "-MMD" :: "-MT" :: file :: arguments_init @ "-o" :: preprocessed_file :: arguments_tl in + let preprocess_arguments = all_cppflags @ "-E" :: arguments_init @ "-o" :: preprocessed_file :: arguments_tl in Filename.quote_command arguments_program preprocess_arguments | _ -> failwith "CompilationDatabase.preprocess: no -o argument value found for " ^ file @@ -89,7 +88,6 @@ let load_and_preprocess ~all_cppflags filename = if GobConfig.get_bool "dbg.verbose" then Printf.printf "Preprocessing %s\n to %s\n using %s\n in %s\n" file preprocessed_file preprocess_command cwd; system ~cwd preprocess_command; (* command/arguments might have paths relative to directory *) - Preprocessor.parse_makefile_deps deps_file; Some preprocessed_file in parse_file filename diff --git a/src/util/dune b/src/util/dune index d8632e1989..72f5b63234 100644 --- a/src/util/dune +++ b/src/util/dune @@ -1,2 +1,2 @@ -(ocamllex oilLexer makefileLexer) -(ocamlyacc oilParser makefileParser) +(ocamllex oilLexer) +(ocamlyacc oilParser) diff --git a/src/util/makefileLexer.mll b/src/util/makefileLexer.mll deleted file mode 100644 index 6eb51caaa6..0000000000 --- a/src/util/makefileLexer.mll +++ /dev/null @@ -1,11 +0,0 @@ -{ - open MakefileParser -} - -rule token = parse - | ' ' { token lexbuf } - | "\\\n" { token lexbuf } - | '\n' { NEWLINE } - | eof { EOF } - | ':' { COLON } - | [^':'' ''\n']+ { IDENTIFIER (Lexing.lexeme lexbuf) } diff --git a/src/util/makefileParser.mly b/src/util/makefileParser.mly deleted file mode 100644 index 6a2946a7d7..0000000000 --- a/src/util/makefileParser.mly +++ /dev/null @@ -1,24 +0,0 @@ -%token IDENTIFIER -%token COLON -%token NEWLINE -%token EOF - -%type deps - -%start deps - -%% - -deps: - | IDENTIFIER COLON identifier_list NEWLINE EOF { ($1, $3) } - ; - -identifier_list: - | { [] } - | identifier_nonempty_list { $1 } - ; - -identifier_nonempty_list: - | IDENTIFIER { [$1] } - | IDENTIFIER identifier_nonempty_list { $1 :: $2 } - ; diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 956bf390fc..d70dbce9a5 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -37,12 +37,4 @@ let cpp = let get_cpp () = Lazy.force cpp -let dependencies: (string, string list) Hashtbl.t = Hashtbl.create 3 - -let parse_makefile_deps makefile = - BatFile.with_file_in makefile (fun input -> - let lexbuf = Lexing.from_channel input in - let (rule, deps) = MakefileParser.deps MakefileLexer.token lexbuf in - let deps = List.remove deps rule in - Hashtbl.replace dependencies rule deps - ) +let dependencies: (string, (string*bool) list) Hashtbl.t = Hashtbl.create 3