From b23d83f2620f09656fdf561caf05548d4a7a4c0f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 10:05:24 +0100 Subject: [PATCH 1/9] Add list of encountered files to CABS and CIL files --- .merlin | 3 ++- src/cil.ml | 4 ++- src/cil.mli | 1 + src/frontc/cabs.ml | 4 +-- src/frontc/cabs2cil.ml | 5 ++-- src/frontc/cabsvisit.ml | 4 +-- src/frontc/clexer.mli | 12 ++++----- src/frontc/cprint.ml | 2 +- src/frontc/frontc.ml | 12 ++++----- src/frontc/patch.ml | 7 +++-- src/mergecil.ml | 7 ++++- src/ocamlutil/errormsg.ml | 12 ++++++--- src/ocamlutil/errormsg.mli | 53 +++++++++++++++++++------------------- 13 files changed, 70 insertions(+), 56 deletions(-) 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..973644637 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -156,6 +156,7 @@ 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 list; } and comment = location * string @@ -5001,7 +5002,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..8ee3afc21 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -93,6 +93,7 @@ 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 list; } (** Top-level representation of a C source file *) diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index fcf015820..20aa621a1 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -189,8 +189,8 @@ 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 furing ptasing *) +and file = string * definition list * string list (* diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 14741e31d..bb0c0bd11 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..b8afa1640 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,14 @@ *) -(* 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 list (* Return the list filenames encountered during lexing *) (* This is the main parser function *) val initial: Lexing.lexbuf -> Cparser.token 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..90eb88645 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 = List.of_seq @@ Hashtbl.to_seq_keys filesH;} + 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..64f439561 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,14 @@ 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; + List.of_seq @@ Hashtbl.to_seq_keys files (* Call this function to announce a new line *) @@ -291,7 +295,9 @@ let setCurrentLine (i: int) = !current.linenum <- i let setCurrentFile (n: string) = - !current.fileName <- cleanFileName n + let cn = cleanFileName n in + Hashtbl.replace files cn (); + !current.fileName <- cleanFileName cn let max_errors = 20 (* Stop after 20 errors *) diff --git a/src/ocamlutil/errormsg.mli b/src/ocamlutil/errormsg.mli index 0792974ad..9fe0f514e 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, @@ -138,19 +138,19 @@ val setCurrentLine: int -> unit val setCurrentFile: string -> 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 list (* Call this function to finish parsing and + * close the input channel, returns a list of + * all encountered filenames *) From b3bfde07bd6a5dcbeb73f9c7a9d08f48a454e5b1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 10:33:06 +0100 Subject: [PATCH 2/9] Ignore line information in formatCIL --- src/formatcil.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 From 2a759462d74aabf33d41e92076ec0e79c51a6c3f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 11:34:18 +0100 Subject: [PATCH 3/9] Compat with OCaml < 4.07 --- src/mergecil.ml | 2 +- src/ocamlutil/errormsg.ml | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/mergecil.ml b/src/mergecil.ml index 90eb88645..a4a36bd1c 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1788,7 +1788,7 @@ let merge (files: file list) (newname: string) : file = globals = revonto (revonto [] !theFile) !theFileTypes; globinit = None; globinitcalled = false; - files = List.of_seq @@ Hashtbl.to_seq_keys filesH;} + 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 diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index 64f439561..2b2f04af4 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -278,7 +278,8 @@ let finishParsing () = let i = !current in (match i.inchan with Some c -> close_in c | _ -> ()); current := dummyinfo; - List.of_seq @@ Hashtbl.to_seq_keys files + (* keys are unique *) + Hashtbl.fold (fun k v acc -> k::acc) files [] (* Call this function to announce a new line *) From 7725b2423b41256419340f8581184f39b76311c3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 12:50:21 +0100 Subject: [PATCH 4/9] Typos & comments --- src/cil.ml | 1 + src/cil.mli | 1 + src/frontc/cabs.ml | 2 +- 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cil.ml b/src/cil.ml index 973644637..20002a046 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -157,6 +157,7 @@ type file = you create a global initialization CIL will try to insert code in main to call it. *) files: string list; + (** A list of those files that were encountered during parsing of this CIL file. *) } and comment = location * string diff --git a/src/cil.mli b/src/cil.mli index 8ee3afc21..f41611c8e 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -94,6 +94,7 @@ type file = * to call it. This will not happen if your file does not contain a * function called "main" *) files: string list; + (** A list of those files that were encountered during parsing of this CIL file. *) } (** Top-level representation of a C source file *) diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index 20aa621a1..977d1cb93 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -189,7 +189,7 @@ and definition = | STATIC_ASSERT of expression * string * cabsloc -(* the string is a file name, then the list of toplevel forms, and finally a list of filenames encountered furing ptasing *) +(* the string is a file name, then the list of toplevel forms, and finally a list of filenames encountered during parsing *) and file = string * definition list * string list From 6d4ca16c2f55b35fee7c312e700578d31c1df8d0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 12:52:00 +0100 Subject: [PATCH 5/9] typo --- src/frontc/clexer.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/frontc/clexer.mli b/src/frontc/clexer.mli index b8afa1640..fa946306a 100644 --- a/src/frontc/clexer.mli +++ b/src/frontc/clexer.mli @@ -43,7 +43,7 @@ val init: filename:string -> Lexing.lexbuf -val finish: unit -> string list (* Return the list filenames encountered during lexing *) +val finish: unit -> string list (* Return the list of filenames encountered during lexing *) (* This is the main parser function *) val initial: Lexing.lexbuf -> Cparser.token @@ -59,4 +59,3 @@ val get_extra_lexeme: unit -> string val clear_white: unit -> unit val clear_lexeme: unit -> unit val currentLoc : unit -> Cabs.cabsloc - From 2788fc81346a516de790119b7b252e4d8ddf42e3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 15:30:04 +0100 Subject: [PATCH 6/9] Formatting Co-authored-by: Simmo Saan --- src/ocamlutil/errormsg.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index 2b2f04af4..7faa83ebc 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -298,7 +298,7 @@ let setCurrentLine (i: int) = let setCurrentFile (n: string) = let cn = cleanFileName n in Hashtbl.replace files cn (); - !current.fileName <- cleanFileName cn + !current.fileName <- cn let max_errors = 20 (* Stop after 20 errors *) From fe7ffcce50d412ff1fda9f7b0027d8a4c7267359 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 15:31:36 +0100 Subject: [PATCH 7/9] Formatting --- src/frontc/cabs2cil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index bb0c0bd11..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; From 4c91e95918f03b4696f4dfb02c7a3dfef2955db9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 4 Feb 2022 13:48:33 +0100 Subject: [PATCH 8/9] Additionally track if an input file is a system header --- src/cil.ml | 5 +++-- src/cil.mli | 5 +++-- src/frontc/cabs.ml | 5 +++-- src/frontc/clexer.mli | 3 ++- src/frontc/clexer.mll | 8 +++----- src/ocamlutil/errormsg.ml | 6 +++--- src/ocamlutil/errormsg.mli | 8 ++++---- 7 files changed, 21 insertions(+), 19 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 20002a046..ee22b4d88 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -156,8 +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 list; - (** A list of those files that were encountered during parsing of this CIL file. *) + 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 diff --git a/src/cil.mli b/src/cil.mli index f41611c8e..d86d08a17 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -93,8 +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 list; - (** A list of those files that were encountered during parsing of this CIL file. *) + 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/frontc/cabs.ml b/src/frontc/cabs.ml index 977d1cb93..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, then the list of toplevel forms, and finally a list of filenames encountered during parsing *) -and file = string * definition list * string 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/clexer.mli b/src/frontc/clexer.mli index fa946306a..85246d5a9 100644 --- a/src/frontc/clexer.mli +++ b/src/frontc/clexer.mli @@ -43,7 +43,8 @@ val init: filename:string -> Lexing.lexbuf -val finish: unit -> string list (* Return the list of filenames encountered during lexing *) +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 diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll index 4507ae42d..adcf356cd 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 '4'); endline lexbuf} | _ {addWhite lexbuf; endline lexbuf} diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index 7faa83ebc..de6e35e67 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -279,7 +279,7 @@ let finishParsing () = (match i.inchan with Some c -> close_in c | _ -> ()); current := dummyinfo; (* keys are unique *) - Hashtbl.fold (fun k v acc -> k::acc) files [] + Hashtbl.fold (fun k v acc -> (k,v)::acc) files [] (* Call this function to announce a new line *) @@ -295,9 +295,9 @@ let newHline () = let setCurrentLine (i: int) = !current.linenum <- i -let setCurrentFile (n: string) = +let setCurrentFile (n: string) (system_header: bool) = let cn = cleanFileName n in - Hashtbl.replace files cn (); + Hashtbl.replace files cn system_header; !current.fileName <- cn diff --git a/src/ocamlutil/errormsg.mli b/src/ocamlutil/errormsg.mli index 9fe0f514e..47561161c 100644 --- a/src/ocamlutil/errormsg.mli +++ b/src/ocamlutil/errormsg.mli @@ -135,7 +135,7 @@ 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 = @@ -170,6 +170,6 @@ val startParsing: ?useBasename:bool -> string -> val startParsingFromString: ?file:string -> ?line:int -> string -> Lexing.lexbuf -val finishParsing: unit -> string list (* Call this function to finish parsing and - * close the input channel, returns a list of - * all encountered filenames *) +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 *) From 908790cb6c85f5ce053a0616bcc6b327758b8966 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 4 Feb 2022 16:31:16 +0100 Subject: [PATCH 9/9] Correct flag for system header is '3' --- src/frontc/clexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll index adcf356cd..b6b7a6a43 100644 --- a/src/frontc/clexer.mll +++ b/src/frontc/clexer.mll @@ -636,7 +636,7 @@ and file = parse | blank {addWhite lexbuf; file lexbuf} | '"' ([^ '\012' '\t' '"']* as filename) '"' ((' ' ['1' -'4'])* as flags) { addWhite lexbuf; (* '"' *) - E.setCurrentFile filename (String.contains flags '4'); + E.setCurrentFile filename (String.contains flags '3'); endline lexbuf} | _ {addWhite lexbuf; endline lexbuf}