diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 39a28b543..4d4334314 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -46,3 +46,10 @@ jobs: - run: opam install . --deps-only --with-doc --with-test - run: opam exec -- dune build - run: opam exec -- dune runtest + + - name: Upload test log + uses: actions/upload-artifact@v3 + if: failure() + with: + name: ${{ matrix.os }}-${{ matrix.ocaml-version }} + path: _build/default/test/cil.log diff --git a/src/cil.ml b/src/cil.ml index f7f26abd1..288c49ce4 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -156,9 +156,6 @@ 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 @@ -5011,8 +5008,7 @@ let dummyFile = { globals = []; fileName = ""; globinit = None; - globinitcalled = false; - files = []; } + globinitcalled = false;} (***** Load and store files as unmarshalled Ocaml binary data. ****) type savedFile = diff --git a/src/cil.mli b/src/cil.mli index b9984a7ce..57d0be532 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -93,9 +93,6 @@ 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/dune b/src/dune index 17022689e..4f3860a09 100644 --- a/src/dune +++ b/src/dune @@ -4,7 +4,7 @@ (public_name goblint-cil) (name cil) (wrapped false) ; this should be changed, but then module paths in goblint need to be prefixed - (libraries zarith findlib dynlink unix str stdlib-shims batteries.unthreaded) + (libraries zarith findlib dynlink unix str stdlib-shims batteries.unthreaded) ; batteries shouldn't be needed, but tests fail on MacOS otherwise: https://github.com/goblint/cil/pull/89#issuecomment-1092610041 (modules (:standard \ main)) ) diff --git a/src/formatcil.ml b/src/formatcil.ml index 563ae4212..01b25f20c 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; - ignore @@ Formatlex.finish (); + Formatlex.finish (); res with Parsing.Parse_error -> begin - ignore @@ Formatlex.finish (); + 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)); - ignore @@ Formatlex.finish (); + Formatlex.finish (); raise e end end diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index 7ce22c1d4..a46cb2e7c 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -189,9 +189,8 @@ 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 whether they are system headers *) -and file = string * definition list * (string * bool) list +(* the string is a file name, and then the list of toplevel forms *) +and file = string * definition list (* diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 302d7d7b9..c6ad353dc 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6897,7 +6897,7 @@ let convFile (f : A.file) : Cil.file = Cil.initCIL (); (* make sure we have initialized CIL *) (* remove parentheses from the Cabs *) - let fname,dl,files = stripParenFile f in + let fname,dl = stripParenFile f in (* Clean up the global types *) initGlobals(); @@ -6986,5 +6986,4 @@ 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 533986f71..a2dd69d1b 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, files): file) : file = - (fname, mapNoCopyList (visitCabsDefinition vis) f, files) +let visitCabsFile (vis: cabsVisitor) ((fname, f): file) : file = + (fname, mapNoCopyList (visitCabsDefinition vis) f) (* end of file *) diff --git a/src/frontc/clexer.mli b/src/frontc/clexer.mli index 85246d5a9..5d90b4ebe 100644 --- a/src/frontc/clexer.mli +++ b/src/frontc/clexer.mli @@ -43,8 +43,7 @@ val init: filename:string -> Lexing.lexbuf -val finish: unit -> (string * bool) list (* Return the list of filenames encountered during lexing - and whether they are system headers *) +val finish: unit -> unit (* 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 13beb6bab..7e1385b20 100644 --- a/src/frontc/clexer.mll +++ b/src/frontc/clexer.mll @@ -659,9 +659,8 @@ and hash = parse E.warn "Bad line number in preprocessed file: %s" s; (-1) in - E.setCurrentLine (lineno - 1); (* A file name may follow *) - file lexbuf } + file (lineno - 1) lexbuf } | "line" { addWhite lexbuf; hash lexbuf } (* MSVC line number info *) (* For pragmas with irregular syntax, like #pragma warning, * we parse them as a whole line. *) @@ -672,15 +671,15 @@ and hash = parse | "pragma" { pragmaLine := true; PRAGMA (currentLoc ()) } | _ { addWhite lexbuf; endline lexbuf} -and file = parse - '\n' {addWhite lexbuf; E.newline (); initial lexbuf} -| blank {addWhite lexbuf; file lexbuf} +and file lineno = parse + '\n' {addWhite lexbuf; E.setCurrent ~file:None ~line:lineno; E.newline (); initial lexbuf} +| blank {addWhite lexbuf; file lineno lexbuf} | '"' ([^ '\012' '\t' '"']* as filename) '"' ((' ' ['1' -'4'])* as flags) { addWhite lexbuf; (* '"' *) - E.setCurrentFile filename (String.contains flags '3'); + E.setCurrent ~file:(Some (filename, String.contains flags '3')) ~line:lineno; endline lexbuf} -| _ {addWhite lexbuf; endline lexbuf} +| _ {addWhite lexbuf; E.setCurrent ~file:None ~line:lineno; endline lexbuf} and endline = parse '\n' { addWhite lexbuf; E.newline (); initial lexbuf} diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 7bbe700ae..fae86f0b4 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -936,7 +936,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 367dc6b0f..52c1cc960 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 ()); - let files = Clexer.finish () in - (fname, cabs, files) + Clexer.finish (); + (fname, cabs) with (Sys_error msg) -> begin ignore (E.log "Cannot open %s : %s\n" fname msg); - ignore @@ Clexer.finish (); + Clexer.finish (); close_output (); raise (ParseError("Cannot open " ^ fname ^ ": " ^ msg ^ "\n")) end | Parsing.Parse_error -> begin ignore (E.log "Parsing error"); - ignore @@ Clexer.finish (); + 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)); - ignore @@ Clexer.finish (); + 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 d3aaaf2ec..6aa5a5730 100644 --- a/src/frontc/patch.ml +++ b/src/frontc/patch.ml @@ -333,8 +333,9 @@ let gettime () : float = let rec applyPatch (patchFile : file) (srcFile : file) : file = begin - let (_, patch, _) = patchFile in - let (srcFname, src, srcFiles) = srcFile in + let patch : definition list = (snd patchFile) in + let srcFname : string = (fst srcFile) in + let src : definition list = (snd srcFile) in (trace "patchTime" (dprintf "applyPatch start: %f\n" (gettime ()))); if (traceActive "patchDebug") then @@ -416,7 +417,7 @@ begin ); (trace "patchTime" (dprintf "applyPatch finish: %f\n" (gettime ()))); - (srcFname, result, srcFiles) + (srcFname, result) end diff --git a/src/mergecil.ml b/src/mergecil.ml index d3b8eaec9..e60e426f5 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1675,11 +1675,6 @@ 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 | x :: t -> revonto (x :: acc) t in let res = @@ -1688,8 +1683,6 @@ globals = revonto (revonto [] !theFile) !theFileTypes; globinit = None; globinitcalled = false; - files = - Hashtbl.fold (fun k v acc -> k :: acc) filesH [] (* keys are unique *); } in init (); diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index de6e35e67..0fcab2388 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -170,8 +170,7 @@ 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 = @@ -257,7 +256,6 @@ let startParsing ?(useBasename=true) (fname: string) = num_errors = 0 } in current := i; - Hashtbl.clear files; lexbuf let startParsingFromString ?(file="") ?(line=1) (str: string) = @@ -271,15 +269,12 @@ 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; - (* keys are unique *) - Hashtbl.fold (fun k v acc -> (k,v)::acc) files [] + current := dummyinfo (* Call this function to announce a new line *) @@ -292,13 +287,19 @@ let newHline () = let i = !current in i.hline <- 1 + i.hline -let setCurrentLine (i: int) = - !current.linenum <- i - -let setCurrentFile (n: string) (system_header: bool) = - let cn = cleanFileName n in - Hashtbl.replace files cn system_header; - !current.fileName <- cn +let transformLocation = ref (fun ~file ~line -> Some (file, line)) + +let setCurrent ~file ~line = + match !transformLocation ~file ~line with + | Some (file, line) -> + begin match file with + | Some (n, system_header) -> + let cn = cleanFileName n in + !current.fileName <- cn + | None -> () + end; + !current.linenum <- line + | None -> () let max_errors = 20 (* Stop after 20 errors *) diff --git a/src/ocamlutil/errormsg.mli b/src/ocamlutil/errormsg.mli index 47561161c..9b29618bc 100644 --- a/src/ocamlutil/errormsg.mli +++ b/src/ocamlutil/errormsg.mli @@ -134,8 +134,8 @@ val getHPosition: unit -> int * string (** high-level position *) val setHLine: int -> unit val setHFile: string -> unit -val setCurrentLine: int -> unit -val setCurrentFile: string -> bool -> unit +val transformLocation: (file:(string * bool) option -> line:int -> ((string * bool) option * int) option) ref +val setCurrent: file:(string * bool) option -> line:int -> unit (** Type for source-file locations *) type location = @@ -170,6 +170,7 @@ val startParsing: ?useBasename:bool -> string -> val startParsingFromString: ?file:string -> ?line:int -> string -> Lexing.lexbuf -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 *) +val finishParsing: unit -> unit (* Call this function to finish parsing and + * close the input channel *) + +