diff --git a/.merlin b/.merlin index 27b68d5aa..0157c75d5 100644 --- a/.merlin +++ b/.merlin @@ -9,4 +9,5 @@ B _build/src/ext/ B _build/src/ext/pta/ B _build/src/frontc/ B _build/src/ocamlutil/ -PKG findlib, zarith +PKG findlib +PKG zarith diff --git a/src/cil.ml b/src/cil.ml index 59b07cf3c..ee22b4d88 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -156,6 +156,9 @@ type file = should always be false if there is no global initializer. When you create a global initialization CIL will try to insert code in main to call it. *) + files: (string * bool) list; + (** A list of those files that were encountered during parsing of this CIL file, + and whether they are system header files *) } and comment = location * string @@ -5001,7 +5004,8 @@ let dummyFile = { globals = []; fileName = ""; globinit = None; - globinitcalled = false;} + globinitcalled = false; + files = []; } (***** Load and store files as unmarshalled Ocaml binary data. ****) type savedFile = diff --git a/src/cil.mli b/src/cil.mli index 45e60e015..d86d08a17 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -93,6 +93,9 @@ type file = * create a global initialization CIL will try to insert code in main * to call it. This will not happen if your file does not contain a * function called "main" *) + files: (string * bool) list; + (** A list of those files that were encountered during parsing of this CIL file, + * and whether they are system header files *) } (** Top-level representation of a C source file *) diff --git a/src/formatcil.ml b/src/formatcil.ml index 01b25f20c..563ae4212 100644 --- a/src/formatcil.ml +++ b/src/formatcil.ml @@ -80,15 +80,15 @@ let doParse (prog: string) Formatparse.initialize Formatlex.initial lexbuf; let res = theParser Formatlex.initial lexbuf in H.add memoTable prog res; - Formatlex.finish (); + ignore @@ Formatlex.finish (); res with Parsing.Parse_error -> begin - Formatlex.finish (); + ignore @@ Formatlex.finish (); E.s (E.error "Parsing error: %s" prog) end | e -> begin ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e)); - Formatlex.finish (); + ignore @@ Formatlex.finish (); raise e end end diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index fcf015820..449f22895 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -189,8 +189,9 @@ and definition = | STATIC_ASSERT of expression * string * cabsloc -(* the string is a file name, and then the list of toplevel forms *) -and file = string * definition list +(* the string is a file name, then the list of toplevel forms, and finally a list of filenames + encountered during parsing and whether they are system headers *) +and file = string * definition list * (string * bool) list (* diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 14741e31d..ebecf88f3 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -5996,7 +5996,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function sformals = []; (* Not final yet *) smaxid = 0; sbody = dummyFunDec.sbody; (* Not final yet *) - smaxstmtid = None; + smaxstmtid = None; sallstmts = []; }; !currentFunctionFDEC.svar.vdecl <- funloc; @@ -6899,7 +6899,7 @@ let convFile (f : A.file) : Cil.file = Cil.initCIL (); (* make sure we have initialized CIL *) (* remove parentheses from the Cabs *) - let fname,dl = stripParenFile f in + let fname,dl,files = stripParenFile f in (* Clean up the global types *) initGlobals(); @@ -6988,4 +6988,5 @@ let convFile (f : A.file) : Cil.file = globals = !globals; globinit = None; globinitcalled = false; + files = files; } diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index a2dd69d1b..533986f71 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -582,7 +582,7 @@ and childrenAttribute vis ((n, el) as input) = and visitCabsAttributes vis (al: attribute list) : attribute list = mapNoCopyList (visitCabsAttribute vis) al -let visitCabsFile (vis: cabsVisitor) ((fname, f): file) : file = - (fname, mapNoCopyList (visitCabsDefinition vis) f) +let visitCabsFile (vis: cabsVisitor) ((fname, f, files): file) : file = + (fname, mapNoCopyList (visitCabsDefinition vis) f, files) (* end of file *) diff --git a/src/frontc/clexer.mli b/src/frontc/clexer.mli index 4dacfb6aa..85246d5a9 100644 --- a/src/frontc/clexer.mli +++ b/src/frontc/clexer.mli @@ -1,11 +1,11 @@ (* * - * Copyright (c) 2001-2002, + * Copyright (c) 2001-2002, * George C. Necula * Scott McPeak * Wes Weimer * All rights reserved. - * + * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: @@ -36,14 +36,15 @@ *) -(* This interface is generated manually. The corresponding .ml file is - * generated automatically and is placed in ../obj/clexer.ml. The reason we - * want this interface is to avoid confusing make with freshly generated +(* This interface is generated manually. The corresponding .ml file is + * generated automatically and is placed in ../obj/clexer.ml. The reason we + * want this interface is to avoid confusing make with freshly generated * interface files *) val init: filename:string -> Lexing.lexbuf -val finish: unit -> unit +val finish: unit -> (string * bool) list (* Return the list of filenames encountered during lexing + and whether they are system headers *) (* This is the main parser function *) val initial: Lexing.lexbuf -> Cparser.token @@ -59,4 +60,3 @@ val get_extra_lexeme: unit -> string val clear_white: unit -> unit val clear_lexeme: unit -> unit val currentLoc : unit -> Cabs.cabsloc - diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll index 4507ae42d..b6b7a6a43 100644 --- a/src/frontc/clexer.mll +++ b/src/frontc/clexer.mll @@ -634,11 +634,9 @@ and hash = parse and file = parse '\n' {addWhite lexbuf; E.newline (); initial lexbuf} | blank {addWhite lexbuf; file lexbuf} -| '"' [^ '\012' '\t' '"']* '"' { addWhite lexbuf; (* '"' *) - let n = Lexing.lexeme lexbuf in - let n1 = String.sub n 1 - ((String.length n) - 2) in - E.setCurrentFile n1; +| '"' ([^ '\012' '\t' '"']* as filename) '"' ((' ' ['1' -'4'])* as flags) + { addWhite lexbuf; (* '"' *) + E.setCurrentFile filename (String.contains flags '3'); endline lexbuf} | _ {addWhite lexbuf; endline lexbuf} diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 0a6397dad..3279ca43a 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -933,7 +933,7 @@ end (* print abstrac_syntax -> () ** Pretty printing the given abstract syntax program. *) -let printFile (result : out_channel) ((fname, defs) : file) = +let printFile (result : out_channel) ((fname, defs, _) : file) = Whitetrack.setOutput result; print_defs defs; Whitetrack.printEOF (); diff --git a/src/frontc/frontc.ml b/src/frontc/frontc.ml index 52c1cc960..367dc6b0f 100644 --- a/src/frontc/frontc.ml +++ b/src/frontc/frontc.ml @@ -188,17 +188,17 @@ and parse_to_cabs_inner (fname : string) = let lexbuf = Clexer.init ~filename:fname in let cabs = Stats.time "parse" (Cparser.interpret (Whitetrack.wraplexer clexer)) lexbuf in Whitetrack.setFinalWhite (Clexer.get_white ()); - Clexer.finish (); - (fname, cabs) + let files = Clexer.finish () in + (fname, cabs, files) with (Sys_error msg) -> begin ignore (E.log "Cannot open %s : %s\n" fname msg); - Clexer.finish (); + ignore @@ Clexer.finish (); close_output (); raise (ParseError("Cannot open " ^ fname ^ ": " ^ msg ^ "\n")) end | Parsing.Parse_error -> begin ignore (E.log "Parsing error"); - Clexer.finish (); + ignore @@ Clexer.finish (); close_output (); (* raise (ParseError("Parse error")) *) let backtrace = Printexc.get_raw_backtrace () in @@ -206,13 +206,13 @@ and parse_to_cabs_inner (fname : string) = end | e -> begin ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e)); - Clexer.finish (); + ignore @@ Clexer.finish (); raise e end (* print to safec.proto.h the prototypes of all functions that are defined *) -let printPrototypes ((fname, file) : Cabs.file) : unit = +let printPrototypes ((fname, file, _) : Cabs.file) : unit = begin (*ignore (E.log "file has %d defns\n" (List.length file));*) diff --git a/src/frontc/patch.ml b/src/frontc/patch.ml index 6aa5a5730..d3aaaf2ec 100644 --- a/src/frontc/patch.ml +++ b/src/frontc/patch.ml @@ -333,9 +333,8 @@ let gettime () : float = let rec applyPatch (patchFile : file) (srcFile : file) : file = begin - let patch : definition list = (snd patchFile) in - let srcFname : string = (fst srcFile) in - let src : definition list = (snd srcFile) in + let (_, patch, _) = patchFile in + let (srcFname, src, srcFiles) = srcFile in (trace "patchTime" (dprintf "applyPatch start: %f\n" (gettime ()))); if (traceActive "patchDebug") then @@ -417,7 +416,7 @@ begin ); (trace "patchTime" (dprintf "applyPatch finish: %f\n" (gettime ()))); - (srcFname, result) + (srcFname, result, srcFiles) end diff --git a/src/mergecil.ml b/src/mergecil.ml index 2da60036b..a4a36bd1c 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1775,6 +1775,9 @@ let merge (files: file list) (newname: string) : file = currentFidx := 0; List.iter (fun f -> oneFilePass2 f; incr currentFidx) files; + let filesH = Hashtbl.create 50 in + List.iter (fun f -> List.iter (fun f -> Hashtbl.replace filesH f ()) f.files) files; + (* Now reverse the result and return the resulting file *) let rec revonto acc = function [] -> acc @@ -1784,7 +1787,9 @@ let merge (files: file list) (newname: string) : file = { fileName = newname; globals = revonto (revonto [] !theFile) !theFileTypes; globinit = None; - globinitcalled = false;} in + globinitcalled = false; + files = Hashtbl.fold (fun k v acc -> k::acc) filesH []; (* keys are unique *)} + in init (); (* Make the GC happy *) (* We have made many renaming changes and sometimes we have just guessed a * name wrong. Make sure now that the local names are unique. *) diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index dadb86494..de6e35e67 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -170,7 +170,8 @@ let theLexbuf = ref (Lexing.from_string "") let fail format = Pretty.gprintf (fun x -> Pretty.fprint stderr ~width:80 x; raise (Failure "")) format - +(***** Keep track of encountered files ******) +let files = Hashtbl.create 10 (***** Handling parsing errors ********) type parseinfo = @@ -256,6 +257,7 @@ let startParsing ?(useBasename=true) (fname: string) = num_errors = 0 } in current := i; + Hashtbl.clear files; lexbuf let startParsingFromString ?(file="") ?(line=1) (str: string) = @@ -269,12 +271,15 @@ let startParsingFromString ?(file="") ?(line=1) (str: string) = num_errors = 0 } in current := i; + Hashtbl.clear files; lexbuf let finishParsing () = let i = !current in (match i.inchan with Some c -> close_in c | _ -> ()); - current := dummyinfo + current := dummyinfo; + (* keys are unique *) + Hashtbl.fold (fun k v acc -> (k,v)::acc) files [] (* Call this function to announce a new line *) @@ -290,8 +295,10 @@ let newHline () = let setCurrentLine (i: int) = !current.linenum <- i -let setCurrentFile (n: string) = - !current.fileName <- cleanFileName n +let setCurrentFile (n: string) (system_header: bool) = + let cn = cleanFileName n in + Hashtbl.replace files cn system_header; + !current.fileName <- cn let max_errors = 20 (* Stop after 20 errors *) diff --git a/src/ocamlutil/errormsg.mli b/src/ocamlutil/errormsg.mli index 0792974ad..47561161c 100644 --- a/src/ocamlutil/errormsg.mli +++ b/src/ocamlutil/errormsg.mli @@ -1,11 +1,11 @@ (* * - * Copyright (c) 2001-2002, + * Copyright (c) 2001-2002, * George C. Necula * Scott McPeak * Wes Weimer * All rights reserved. - * + * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: @@ -40,7 +40,7 @@ val logChannel : out_channel ref (** If set then print debugging info *) -val debugFlag : bool ref +val debugFlag : bool ref val verboseFlag : bool ref @@ -63,12 +63,12 @@ val warnFlag: bool ref exception Error - (* Error reporting. All of these functions take same arguments as a - * Pretty.eprintf. They set the hadErrors flag, but do not raise an + (* Error reporting. All of these functions take same arguments as a + * Pretty.eprintf. They set the hadErrors flag, but do not raise an * exception. Their return type is unit. *) -(** Prints an error message of the form [Error: ...]. +(** Prints an error message of the form [Error: ...]. Use in conjunction with s, for example: [E.s (E.error ... )]. *) val error: ('a,unit,Pretty.doc,unit) format4 -> 'a @@ -83,13 +83,13 @@ val s: 'a -> 'b (** This is set whenever one of the above error functions are called. It must be cleared manually *) -val hadErrors: bool ref +val hadErrors: bool ref -(** Like {!Errormsg.error} but does not raise the {!Errormsg.Error} +(** Like {!Errormsg.error} but does not raise the {!Errormsg.Error} * exception. Return type is unit. *) val warn: ('a,unit,Pretty.doc,unit) format4 -> 'a -(** Like {!Errormsg.warn} but optional. Printed only if the +(** Like {!Errormsg.warn} but optional. Printed only if the * {!Errormsg.warnFlag} is set *) val warnOpt: ('a,unit,Pretty.doc,unit) format4 -> 'a @@ -99,10 +99,10 @@ val log: ('a,unit,Pretty.doc,unit) format4 -> 'a (** same as {!Errormsg.log} but do not wrap lines *) val logg: ('a,unit,Pretty.doc,unit) format4 -> 'a - (* All of the error and warning reporting functions can also print a - * context. To register a context printing function use "pushContext". To - * remove the last registered one use "popContext". If one of the error - * reporting functions is called it will invoke all currently registered + (* All of the error and warning reporting functions can also print a + * context. To register a context printing function use "pushContext". To + * remove the last registered one use "popContext". If one of the error + * reporting functions is called it will invoke all currently registered * context reporting functions in the reverse order they were registered. *) (** Do not actually print (i.e. print to /dev/null) *) @@ -117,14 +117,14 @@ val popContext : unit -> unit (** Show the context stack to stderr *) val showContext : unit -> unit -(** To ensure that the context is registered and removed properly, use the +(** To ensure that the context is registered and removed properly, use the function below *) val withContext : (unit -> Pretty.doc) -> ('a -> 'b) -> 'a -> 'b val newline: unit -> unit (* Call this function to announce a new line *) -val newHline: unit -> unit +val newHline: unit -> unit val getPosition: unit -> int * string * int * int (* Line number, file name, current byte count in file, @@ -135,22 +135,22 @@ val setHLine: int -> unit val setHFile: string -> unit val setCurrentLine: int -> unit -val setCurrentFile: string -> unit +val setCurrentFile: string -> bool -> unit (** Type for source-file locations *) -type location = +type location = { file: string; (** The file name *) line: int; (** The line number *) hfile: string; (** The high-level file name, or "" if not present *) hline: int; (** The high-level line number, or 0 if not present *) - } + } val d_loc: unit -> location -> Pretty.doc val d_hloc: unit -> location -> Pretty.doc - + val getLocation: unit -> location -val parse_error: string -> (* A message *) +val parse_error: string -> (* A message *) 'a (** An unknown location for use when you need one but you don't have one *) @@ -161,16 +161,15 @@ val locUnknown: location val readingFromStdin: bool ref -(* Call this function to start parsing. useBasename is by default "true", - * meaning that the error information maintains only the basename. If the +(* Call this function to start parsing. useBasename is by default "true", + * meaning that the error information maintains only the basename. If the * file name is - then it reads from stdin. *) -val startParsing: ?useBasename:bool -> string -> - Lexing.lexbuf +val startParsing: ?useBasename:bool -> string -> + Lexing.lexbuf val startParsingFromString: ?file:string -> ?line:int -> string -> Lexing.lexbuf -val finishParsing: unit -> unit (* Call this function to finish parsing and - * close the input channel *) - - +val finishParsing: unit -> (string * bool) list (* Call this function to finish parsing and + * close the input channel, returns a list of all + * encountered filenames and whether they are system headers *)