aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/AsmToJSON.ml2
-rw-r--r--cfrontend/C2C.ml35
-rw-r--r--cfrontend/CPragmas.ml2
-rw-r--r--cparser/Bitfields.ml2
-rw-r--r--cparser/Checks.ml2
-rw-r--r--cparser/Cutil.ml2
-rw-r--r--cparser/Diagnostics.ml (renamed from cparser/Cerrors.ml)19
-rw-r--r--cparser/Diagnostics.mli (renamed from cparser/Cerrors.mli)10
-rw-r--r--cparser/Elab.ml4
-rw-r--r--cparser/ExtendedAsm.ml4
-rw-r--r--cparser/Lexer.mll10
-rw-r--r--cparser/PackedStructs.ml2
-rw-r--r--cparser/Parse.ml15
-rw-r--r--cparser/Parse.mli2
-rw-r--r--cparser/Rename.ml2
-rw-r--r--cparser/Unblock.ml3
-rw-r--r--driver/Assembler.ml4
-rw-r--r--driver/Commandline.ml25
-rw-r--r--driver/Commandline.mli11
-rw-r--r--driver/Driver.ml46
-rw-r--r--driver/Driveraux.ml25
-rw-r--r--driver/Driveraux.mli4
-rw-r--r--driver/Frontend.ml15
-rw-r--r--driver/Linker.ml4
-rw-r--r--exportclight/Clightgen.ml33
-rw-r--r--powerpc/AsmToJSON.ml2
26 files changed, 147 insertions, 138 deletions
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index fadcdf58..49cca929 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -154,7 +154,7 @@ let pp_instructions pp ic =
begin match ef with
| EF_inline_asm _ ->
instruction pp "Pinlineasm" [Id];
- Cerrors.warning ("", -10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump"
+ Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump")
| EF_annot (kind,txt, targs) ->
let annot_string = PrintAsmaux.annot_text TargetPrinter.preg_annot "r1" (camlstring_of_coqstring txt) args in
let len = String.length annot_string in
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 743ffd3b..6a2c6a4e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -120,13 +120,16 @@ let currentLocation = ref Cutil.no_loc
let updateLoc l = currentLocation := l
let error fmt =
- Cerrors.error !currentLocation fmt
+ Diagnostics.error !currentLocation fmt
+
+let fatal_error fmt =
+ Diagnostics.fatal_error !currentLocation fmt
let unsupported msg =
- Cerrors.error !currentLocation "unsupported feature: %s" msg
+ Diagnostics.error !currentLocation "unsupported feature: %s" msg
let warning t msg =
- Cerrors.warning !currentLocation t msg
+ Diagnostics.warning !currentLocation t msg
let string_of_errmsg msg =
let string_of_err = function
@@ -657,11 +660,11 @@ let checkFloatOverflow f typ =
match f with
| Fappli_IEEE.B754_finite _ -> ()
| Fappli_IEEE.B754_zero _ ->
- warning Cerrors.Literal_range "magnitude of floating-point constant too small for type '%s'" typ
+ warning Diagnostics.Literal_range "magnitude of floating-point constant too small for type '%s'" typ
| Fappli_IEEE.B754_infinity _ ->
- warning Cerrors.Literal_range "magnitude of floating-point constant too large for type '%s'" typ
+ warning Diagnostics.Literal_range "magnitude of floating-point constant too large for type '%s'" typ
| Fappli_IEEE.B754_nan _ ->
- warning Cerrors.Literal_range "floating-point converts converts to 'NaN'"
+ warning Diagnostics.Literal_range "floating-point converts converts to 'NaN'"
let convertFloat f kind =
let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in
@@ -783,7 +786,7 @@ let rec convertExpr env e =
let e2' = convertExpr env e2 in
if Cutil.is_composite_type env e1.etyp
&& List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then
- warning Cerrors.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored";
+ warning Diagnostics.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored";
ewrap (Ctyping.eassign e1' e2')
| C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign|
C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign|
@@ -1080,7 +1083,7 @@ let rec convertStmt env s =
| _ -> Cutil.is_debug_stmt s in
if init.sdesc <> C.Sskip && not (init_debug init) then
begin
- warning Cerrors.Unnamed "ignored code at beginning of 'switch'";
+ warning Diagnostics.Unnamed "ignored code at beginning of 'switch'";
contains_case init
end;
let te = convertExpr env e in
@@ -1276,7 +1279,7 @@ let rec convertGlobdecls env res gl =
begin match Cutil.unroll env ty with
| TFun(tres, targs, va, a) ->
if targs = None then
- warning Cerrors.Unnamed "'%s' is declared without a function prototype" id.name;
+ warning Diagnostics.Unnamed "'%s' is declared without a function prototype" id.name;
convertGlobdecls env (convertFundecl env d :: res) gl'
| _ ->
convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl'
@@ -1290,7 +1293,7 @@ let rec convertGlobdecls env res gl =
convertGlobdecls env res gl'
| C.Gpragma s ->
if not (!process_pragma_hook s) then
- warning Cerrors.Unknown_pragmas "unknown pragma ignored";
+ warning Diagnostics.Unknown_pragmas "unknown pragma ignored";
convertGlobdecls env res gl'
(** Convert struct and union declarations.
@@ -1388,7 +1391,7 @@ let public_globals gl =
(** Convert a [C.program] into a [Csyntax.program] *)
let convertProgram p =
- Cerrors.reset();
+ Diagnostics.reset();
stringNum := 0;
Hashtbl.clear decl_atom;
Hashtbl.clear stringTable;
@@ -1399,9 +1402,8 @@ let convertProgram p =
let typs = convertCompositedefs env [] p in
match build_composite_env typs with
| Errors.Error msg ->
- error "incorrect struct or union definition: %s"
- (string_of_errmsg msg);
- None
+ fatal_error "incorrect struct or union definition: %s"
+ (string_of_errmsg msg)
| Errors.OK ce ->
comp_env := ce;
let gl1 = convertGlobdecls env [] p in
@@ -1413,6 +1415,7 @@ let convertProgram p =
prog_main = intern_string "main";
prog_types = typs;
prog_comp_env = ce } in
- if Cerrors.check_errors () then None else Some p'
+ Diagnostics.check_errors ();
+ p'
with Env.Error msg ->
- error "%s" (Env.error_message msg); None
+ fatal_error "%s" (Env.error_message msg)
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index d61af920..44660718 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -72,7 +72,7 @@ let process_pragma name =
| "section" :: _ ->
C2C.error "ill-formed `section' pragma"; true
| "use_section" :: classname :: identlist ->
- if identlist = [] then C2C.warning Cerrors.Unnamed "empty `use_section' pragma";
+ if identlist = [] then C2C.warning Diagnostics.Unnamed "empty `use_section' pragma";
List.iter (process_use_section_pragma classname) identlist;
true
| "use_section" :: _ ->
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 35da5d4e..e0dccbd2 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -66,7 +66,7 @@ let is_signed_enum_bitfield env sid fld eid n =
else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members
then true
else begin
- Cerrors.warning Cutil.no_loc Cerrors.Unnamed
+ Diagnostics.warning Diagnostics.no_loc Diagnostics.Unnamed
"not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)"
eid.C.name fld sid.C.name n;
false
diff --git a/cparser/Checks.ml b/cparser/Checks.ml
index 073d1057..ee36e226 100644
--- a/cparser/Checks.ml
+++ b/cparser/Checks.ml
@@ -14,7 +14,7 @@
(* *********************************************************************)
open C
-open Cerrors
+open Diagnostics
open Cutil
open Env
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 9bc11141..71c253f8 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -15,7 +15,7 @@
(* Operations on C types and abstract syntax *)
-open Cerrors
+open Diagnostics
open C
open Env
open Machine
diff --git a/cparser/Cerrors.ml b/cparser/Diagnostics.ml
index 34fc4fcf..d9b96393 100644
--- a/cparser/Cerrors.ml
+++ b/cparser/Diagnostics.ml
@@ -299,11 +299,13 @@ let parse_loc_format s =
(* Print the location or ccomp for the case of unknown loc *)
let pp_loc fmt (filename,lineno) =
- if filename <> "" && lineno <> -10 && filename <> "cabs loc unknown" then
+ let lineno = if lineno = -10 then "" else
match !diagnostics_format with
- | Default -> fprintf fmt "%t%s:%d:%t " bc filename lineno rsc
- | MSVC -> fprintf fmt "%t%s(%d):%t " bc filename lineno rsc
- | Vi -> fprintf fmt "%t%s +%d:%t " bc filename lineno rsc
+ | Default -> sprintf ":%d" lineno
+ | MSVC -> sprintf "(%d)" lineno
+ | Vi -> sprintf " +%d" lineno in
+ if filename <> "" && filename <> "cabs loc unknown" then
+ fprintf fmt "%t%s%s:%t " bc filename lineno rsc
else
fprintf fmt "%tccomp:%t " bc rsc
@@ -341,11 +343,12 @@ let fatal_error loc fmt =
fatal_error None loc fmt
let check_errors () =
- if !num_errors > 0 then
+ if !num_errors > 0 then begin
eprintf "@[<hov 0>%d error%s detected.@]@."
!num_errors
(if !num_errors = 1 then "" else "s");
- !num_errors > 0
+ raise Abort
+ end
let error_option w =
let key = string_of_warning w in
@@ -428,3 +431,7 @@ let crash exn =
eprintf "Fatal error: uncaught exception %s\n%s" exc backtrace;
exit 2
end
+
+let no_loc = ("", -1)
+
+let file_loc file = (file,-10)
diff --git a/cparser/Cerrors.mli b/cparser/Diagnostics.mli
index c351443c..54395136 100644
--- a/cparser/Cerrors.mli
+++ b/cparser/Diagnostics.mli
@@ -21,8 +21,8 @@ val reset : unit -> unit
exception Abort
(** Exception raised upon fatal errors *)
-val check_errors : unit -> bool
- (** Check whether errors occured *)
+val check_errors : unit -> unit
+ (** Check whether errors occured and raise abort if an error occured *)
type warning_type =
| Unnamed (** warnings which cannot be turned off *)
@@ -78,3 +78,9 @@ val raise_on_errors : unit -> unit
val crash: exn -> unit
(** Report the backtrace of the last exception and exit *)
+
+val no_loc : string * int
+(** Location used for unknown locations *)
+
+val file_loc : string -> string * int
+(** [file_loc f] generates a location for file [f] *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 86e71865..4de43fe0 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -20,8 +20,8 @@
open Machine
open Cabs
open C
-open Cerrors
-open Cutil
+open Diagnostics
+open !Cutil
(** * Utility functions *)
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 30d1a0cc..6cd95aec 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -33,7 +33,7 @@ open Printf
open Machine
open C
open Cutil
-open Cerrors
+open Diagnostics
(* Renaming of labeled and numbered operands *)
@@ -176,7 +176,7 @@ let rename_placeholders loc template subst =
try
StringMap.find p subst
with Not_found ->
- error loc"'%s' in asm text does not designate any operand" p;
+ error loc "'%s' in asm text does not designate any operand" p;
"%<error>"
in
Str.global_substitute re_asm_placeholder
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index ec344f7a..cf8788c5 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -126,16 +126,16 @@ let currentLoc =
(* Error reporting *)
let fatal_error lb fmt =
- Cerrors.fatal_error
+ Diagnostics.fatal_error
(lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt
let error lb fmt =
- Cerrors.error
+ Diagnostics.error
(lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) fmt
let warning lb fmt =
- Cerrors.warning
- (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Cerrors.Unnamed ("warning: " ^^ fmt)
+ Diagnostics.warning
+ (lb.lex_curr_p.pos_fname,lb.lex_curr_p.pos_lnum) Diagnostics.Unnamed ("warning: " ^^ fmt)
(* Simple character escapes *)
@@ -483,7 +483,7 @@ and singleline_comment = parse
and supplier = I.lexer_lexbuf_to_supplier lexer lexbuf
and succeed () = ()
and fail checkpoint =
- Cerrors.fatal_error_raw "%s" (ErrorReports.report text !buffer checkpoint)
+ Diagnostics.fatal_error_raw "%s" (ErrorReports.report text !buffer checkpoint)
in
I.loop_handle succeed fail supplier checkpoint
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index b74a29d4..e1287eb8 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -23,7 +23,7 @@ open Machine
open C
open Cutil
open Env
-open Cerrors
+open Diagnostics
open Transform
(* The set of struct fields that are byte-swapped.
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index ecd13332..8665e158 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -46,7 +46,7 @@ let read_file sourcefile =
text
let preprocessed_file transfs name sourcefile =
- Cerrors.reset();
+ Diagnostics.reset();
(* Reading the whole file at once may seem costly, but seems to be
the simplest / most robust way of accessing the text underlying
a range of positions. This is used when printing an error message.
@@ -55,7 +55,6 @@ let preprocessed_file transfs name sourcefile =
on my machine. *)
let text = read_file sourcefile in
let p =
- try
let t = parse_transformations transfs in
let rec inf = Datatypes.S inf in
let ast : Cabs.definition list =
@@ -70,13 +69,11 @@ let preprocessed_file transfs name sourcefile =
| Parser.Parser.Inter.Fail_pr ->
(* Theoretically impossible : implies inconsistencies
between grammars. *)
- Cerrors.fatal_error Cutil.no_loc "Internal error while parsing"
+ Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing"
| Parser.Parser.Inter.Timeout_pr -> assert false
| Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in
let p1 = Timing.time "Elaboration" Elab.elab_file ast in
- Cerrors.raise_on_errors ();
- Timing.time2 "Emulations" transform_program t p1 name
- with
- | Cerrors.Abort ->
- [] in
- if Cerrors.check_errors() then None else Some p
+ Diagnostics.check_errors ();
+ Timing.time2 "Emulations" transform_program t p1 name in
+ Diagnostics.check_errors();
+ p
diff --git a/cparser/Parse.mli b/cparser/Parse.mli
index 58c3cfb9..433e2e73 100644
--- a/cparser/Parse.mli
+++ b/cparser/Parse.mli
@@ -15,7 +15,7 @@
(* Entry point for the library: parse, elaborate, and transform *)
-val preprocessed_file: string -> string -> string -> C.program option
+val preprocessed_file: string -> string -> string -> C.program
(* first arg: desired transformations
second arg: source file name before preprocessing
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index f402ea39..cdb5751e 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -83,7 +83,7 @@ let ident env id =
try
IdentMap.find id env.re_id
with Not_found ->
- Cerrors.fatal_error no_loc "internal error: rename: %s__%d unbound"
+ Diagnostics.fatal_error Diagnostics.no_loc "internal error: rename: %s__%d unbound"
id.name id.stamp
let rec typ env = function
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 91e2ce20..5df2e2cf 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -20,7 +20,6 @@
open C
open Cutil
-open Cerrors
(* Convert an initializer to a list of assignment expressions. *)
@@ -32,7 +31,7 @@ let rec local_initializer env path init k =
let (ty_elt, sz) =
match unroll env path.etyp with
| TArray(ty_elt, Some sz, _) -> (ty_elt, sz)
- | _ -> fatal_error no_loc "Wrong type for array initializer" in
+ | _ -> Diagnostics.fatal_error Diagnostics.no_loc "Wrong type for array initializer" in
let rec array_init pos il =
if pos >= sz then k else begin
let (i1, il') =
diff --git a/driver/Assembler.ml b/driver/Assembler.ml
index ba9351ca..1694dfa8 100644
--- a/driver/Assembler.ml
+++ b/driver/Assembler.ml
@@ -18,6 +18,7 @@ open Driveraux
(* From asm to object file *)
let assemble ifile ofile =
+ Diagnostics.raise_on_errors ();
let cmd = List.concat [
Configuration.asm;
["-o"; ofile];
@@ -27,8 +28,7 @@ let assemble ifile ofile =
let exc = command cmd in
if exc <> 0 then begin
safe_remove ofile;
- command_error "assembler" exc;
- exit 2
+ command_error "assembler" exc
end
let assembler_actions =
diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index 035c33e0..f139212d 100644
--- a/driver/Commandline.ml
+++ b/driver/Commandline.ml
@@ -35,6 +35,8 @@ type action =
| Ignore
| Unit of (unit -> unit)
+exception CmdError of string
+
let match_pattern text = function
| Exact s ->
text = s
@@ -72,7 +74,8 @@ let parse_array spec argv first last =
with Not_found -> find_action s inexact_cases in
match optact with
| None ->
- eprintf "Unknown argument `%s'\n" s; exit 2
+ let msg = sprintf "Unknown argument `%s'" s in
+ raise (CmdError msg)
| Some(Set r) ->
r := true; parse (i+1)
| Some(Unset r) ->
@@ -83,7 +86,8 @@ let parse_array spec argv first last =
if i + 1 <= last then begin
fn argv.(i+1); parse (i+2)
end else begin
- eprintf "Option `%s' expects an argument\n" s; exit 2
+ let msg = sprintf "Option `%s' expects an argument" s in
+ raise (CmdError msg)
end
| Some(Integer fn) ->
if i + 1 <= last then begin
@@ -91,18 +95,20 @@ let parse_array spec argv first last =
try
int_of_string argv.(i+1)
with Failure _ ->
- eprintf "Argument to option `%s' must be an integer\n" s;
- exit 2
+ let msg = sprintf "Argument to option `%s' must be an integer" s in
+ raise (CmdError msg)
in
fn n; parse (i+2)
end else begin
- eprintf "Option `%s' expects an argument\n" s; exit 2
+ let msg = sprintf "Option `%s' expects an argument" s in
+ raise (CmdError msg)
end
| Some (Ignore) ->
if i + 1 <= last then begin
parse (i+2)
end else begin
- eprintf "Option `%s' expects an argument\n" s; exit 2
+ let msg = sprintf "Option `%s' expects an argument" s in
+ raise (CmdError msg)
end
| Some (Unit f) -> f (); parse (i+1)
end
@@ -115,8 +121,7 @@ let parse_cmdline spec =
argv := expandargv Sys.argv;
parse_array spec !argv 1 (Array.length !argv - 1)
with Responsefile.Error s ->
- eprintf "%s" s;
- exit 2
+ raise (CmdError s)
let long_int_action key s =
let ls = String.length s
@@ -126,8 +131,8 @@ let long_int_action key s =
try
int_of_string s
with Failure _ ->
- eprintf "Argument to option `%s' must be an integer\n" key;
- exit 2
+ let msg = sprintf "Argument to option `%s' must be an integer" key in
+ raise (CmdError msg)
let longopt_int key f =
let act s =
diff --git a/driver/Commandline.mli b/driver/Commandline.mli
index 32f5daf3..e1b917f2 100644
--- a/driver/Commandline.mli
+++ b/driver/Commandline.mli
@@ -35,12 +35,17 @@ type action =
| Integer of (int -> unit) (** read next arg as an int, call function *)
| Ignore (** ignore the next arg *)
| Unit of (unit -> unit) (** call the function with unit as argument *)
-
-val parse_cmdline: (pattern * action) list -> unit
-
(* Note on precedence: [Exact] patterns are tried first, then the other
patterns are tried in the order in which they appear in the list. *)
+exception CmdError of string
+(** Raise by [parse_cmdline] when an error occured *)
+
+val parse_cmdline: (pattern * action) list -> unit
+(** [parse_cmdline actions] parses the commandline and performs all [actions].
+ Raises [CmdError] if an error occurred.
+*)
+
val longopt_int: string -> (int -> unit) -> pattern * action
(** [longopt_int key fn] generates a pattern and an action for
options of the form [key=<n>] and calls [fn] with the integer argument
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 063e49d2..9c9f2d79 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -19,6 +19,7 @@ open Driveraux
open Frontend
open Assembler
open Linker
+open Diagnostics
(* Name used for version string etc. *)
let tool_name = "C verified compiler"
@@ -61,8 +62,8 @@ let compile_c_file sourcename ifile ofile =
| Errors.OK asm ->
asm
| Errors.Error msg ->
- eprintf "%s: %a" sourcename print_error msg;
- exit 2 in
+ let loc = file_loc sourcename in
+ fatal_error loc "%a" print_error msg in
(* Dump Asm in binary and JSON format *)
AsmToJSON.print_if asm sourcename;
(* Print Asm in text form *)
@@ -143,10 +144,8 @@ let process_h_file sourcename =
ensure_inputfile_exists sourcename;
preprocess sourcename (output_filename_default "-");
""
- end else begin
- eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename;
- exit 2
- end
+ end else
+ fatal_error no_loc "input file %s ignored (not in -E mode)\n" sourcename
let target_help =
if Configuration.arch = "arm" && Configuration.model <> "armv6" then
@@ -223,7 +222,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
-sdump Save info for post-linking validation in <file>.json
|} ^
general_help ^
- Cerrors.warning_help ^
+ warning_help ^
{|Interpreter mode:
-interp Execute given .c files using the reference interpreter
-quiet Suppress diagnostic messages for the interpreter
@@ -237,10 +236,9 @@ let print_usage_and_exit () =
let enforce_buildnr nr =
let build = int_of_string Version.buildnr in
- if nr != build then begin
- eprintf "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\
-Please use matching builds of QSK and CompCert.\n" build nr; exit 2
- end
+ if nr != build then
+ fatal_error no_loc "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\
+Please use matching builds of QSK and CompCert." build nr
let dump_mnemonics destfile =
let oc = open_out_bin destfile in
@@ -349,7 +347,7 @@ let cmdline_actions =
(* General options *)
general_options @
(* Diagnostic options *)
- Cerrors.warning_options @
+ warning_options @
(* Interpreter mode *)
[ Exact "-interp", Set option_interp;
Exact "-quiet", Unit (fun () -> Interp.trace := 0);
@@ -371,7 +369,7 @@ let cmdline_actions =
@ [
(* Catch options that are not handled *)
Prefix "-", Self (fun s ->
- eprintf "Unknown option `%s'\n" s; exit 2);
+ fatal_error no_loc "Unknown option `%s'" s);
(* File arguments *)
Suffix ".c", Self (fun s ->
push_action process_c_file s; incr num_source_files; incr num_input_files);
@@ -405,21 +403,17 @@ let _ =
Frontend.init ();
parse_cmdline cmdline_actions;
DebugInit.init (); (* Initialize the debug functions *)
- if nolink () && !option_o <> None && !num_source_files >= 2 then begin
- eprintf "Ambiguous '-o' option (multiple source files)\n";
- exit 2
- end;
+ if nolink () && !option_o <> None && !num_source_files >= 2 then
+ fatal_error no_loc "Ambiguous '-o' option (multiple source files)";
if !num_input_files = 0 then
- begin
- eprintf "ccomp: error: no input file\n";
- exit 2
- end;
+ fatal_error no_loc "no input file";
let linker_args = time "Total compilation time" perform_actions () in
if not (nolink ()) && linker_args <> [] then begin
linker (output_filename_default "a.out") linker_args
end;
- if Cerrors.check_errors () then exit 2
- with Sys_error msg ->
- eprintf "I/O error: %s.\n" msg; exit 2
- | e ->
- Cerrors.crash e
+ check_errors ()
+ with
+ | Sys_error msg
+ | CmdError msg -> error no_loc "%s" msg; exit 2
+ | Abort -> exit 2
+ | e -> crash e
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 6d8d0adc..ccc3d00d 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -13,6 +13,7 @@
open Printf
open Clflags
+open Diagnostics
(* Safe removal of files *)
let safe_remove file =
@@ -46,9 +47,9 @@ let command stdout args =
match status with
| Unix.WEXITED rc -> rc
| Unix.WSIGNALED n | Unix.WSTOPPED n ->
- eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
+ error no_loc "Command '%s' killed on a signal." argv.(0); -1
with Unix.Unix_error(err, fn, param) ->
- eprintf "Error executing '%s': %s: %s %s\n"
+ error no_loc "executing '%s': %s: %s %s"
argv.(0) fn (Unix.error_message err) param;
-1
@@ -81,7 +82,7 @@ let command ?stdout args =
command stdout args
let command_error n exc =
- eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc
+ fatal_error no_loc "%s command failed with exit code %d (use -v to see invocation)\n" n exc
(* Determine names for output files. We use -o option if specified
@@ -105,20 +106,18 @@ let output_filename_default default_file =
(* All input files should exist *)
let ensure_inputfile_exists name =
- if not (Sys.file_exists name) then begin
- eprintf "error: no such file or directory: '%s'\n" name;
- exit 2
- end
+ if not (Sys.file_exists name) then
+ fatal_error no_loc "no such file or directory: '%s'" name
+
(* Printing of error messages *)
-let print_error oc msg =
+let print_error pp msg =
let print_one_error = function
- | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
- | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
- | Errors.POS i -> fprintf oc "%ld" (Camlcoq.P.to_int32 i)
+ | Errors.MSG s -> Format.pp_print_string pp (Camlcoq.camlstring_of_coqstring s)
+ | Errors.CTX i -> Format.pp_print_string pp (Camlcoq.extern_atom i)
+ | Errors.POS i -> Format.fprintf pp "%ld" (Camlcoq.P.to_int32 i)
in
- List.iter print_one_error msg;
- output_char oc '\n'
+ List.iter print_one_error msg
(* Command-line parsing *)
let explode_comma_option s =
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli
index 51333b2a..6f0eaddb 100644
--- a/driver/Driveraux.mli
+++ b/driver/Driveraux.mli
@@ -16,7 +16,7 @@ val command: ?stdout:string -> string list -> int
(** Execute the command with the given arguments and an optional file for
the stdout. Returns the exit code. *)
-val command_error: string -> int -> unit
+val command_error: string -> int -> 'a
(** Generate an error message for the given command and exit code *)
val safe_remove: string -> unit
@@ -38,7 +38,7 @@ val output_filename_default: string -> string
val ensure_inputfile_exists: string -> unit
(** Test whether the given input file exists *)
-val print_error:out_channel -> Errors.errcode list -> unit
+val print_error:Format.formatter -> Errors.errcode list -> unit
(** Printing of error messages *)
val explode_comma_option: string -> string list
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 2b9d5860..2bc4f844 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -14,7 +14,6 @@
open Clflags
open Commandline
open Driveraux
-open Printf
(* Common frontend functions between clightgen and ccomp *)
@@ -22,6 +21,7 @@ open Printf
(* From C to preprocessed C *)
let preprocess ifile ofile =
+ Diagnostics.raise_on_errors ();
let output =
if ofile = "-" then None else Some ofile in
let cmd = List.concat [
@@ -37,8 +37,6 @@ let preprocess ifile ofile =
if exc <> 0 then begin
if ofile <> "-" then safe_remove ofile;
command_error "preprocessor" exc;
- eprintf "Error during preprocessing.\n";
- exit 2
end
(* From preprocessed C to Csyntax *)
@@ -54,18 +52,11 @@ let parse_c_file sourcename ifile =
^ (if !option_fpacked_structs then "p" else "")
in
(* Parsing and production of a simplified C AST *)
- let ast =
- match Parse.preprocessed_file simplifs sourcename ifile with
- | None -> exit 2
- | Some p -> p in
+ let ast = Parse.preprocessed_file simplifs sourcename ifile in
(* Save C AST if requested *)
Cprint.print_if ast;
(* Conversion to Csyntax *)
- let csyntax =
- match Timing.time "CompCert C generation" C2C.convertProgram ast with
- | None -> exit 2
- | Some p -> p in
- flush stderr;
+ let csyntax = Timing.time "CompCert C generation" C2C.convertProgram ast in
(* Save CompCert C AST if requested *)
PrintCsyntax.print_if csyntax;
csyntax
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 37a5cde0..6e6ad6b4 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -19,6 +19,7 @@ open Driveraux
(* Linking *)
let linker exe_name files =
+ Diagnostics.raise_on_errors ();
let cmd = List.concat [
Configuration.linker;
["-o"; exe_name];
@@ -29,8 +30,7 @@ let linker exe_name files =
] in
let exc = command cmd in
if exc <> 0 then begin
- command_error "linker" exc;
- exit 2
+ command_error "linker" exc
end
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 2878cb17..9cb0674e 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -19,6 +19,7 @@ open Clflags
open CommonOptions
open Driveraux
open Frontend
+open Diagnostics
let tool_name = "Clight generator"
@@ -29,6 +30,7 @@ let option_normalize = ref false
(* From CompCert C AST to Clight *)
let compile_c_ast sourcename csyntax ofile =
+ let loc = file_loc sourcename in
let clight =
match SimplExpr.transl_program csyntax with
| Errors.OK p ->
@@ -38,12 +40,10 @@ let compile_c_ast sourcename csyntax ofile =
then Clightnorm.norm_program p'
else p'
| Errors.Error msg ->
- print_error stderr msg;
- exit 2
+ fatal_error loc "%a" print_error msg
end
| Errors.Error msg ->
- print_error stderr msg;
- exit 2 in
+ fatal_error loc "%a" print_error msg in
(* Dump Clight in C syntax if requested *)
if !option_dclight then begin
let ofile = Filename.chop_suffix sourcename ".c" ^ ".light.c" in
@@ -104,7 +104,8 @@ language_support_help ^
-dclight Save generated Clight in <file>.light.c
|} ^
general_help ^
- Cerrors.warning_help
+ warning_help
+
let print_usage_and_exit () =
printf "%s" usage_string; exit 0
@@ -145,11 +146,11 @@ let cmdline_actions =
Exact "-dclight", Set option_dclight;]
@ general_options
(* Diagnostic options *)
- @ Cerrors.warning_options
+ @ warning_options
@ language_support_options @
(* Catch options that are not handled *)
[Prefix "-", Self (fun s ->
- eprintf "Unknown option `%s'\n" s; exit 2);
+ fatal_error no_loc "Unknown option `%s'" s);
(* File arguments *)
Suffix ".c", Self (fun s ->
incr num_input_files; push_action process_c_file s);
@@ -160,6 +161,7 @@ let cmdline_actions =
]
let _ =
+ try
Gc.set { (Gc.get()) with
Gc.minor_heap_size = 524288; (* 512k *)
Gc.major_heap_increment = 4194304 (* 4M *)
@@ -167,12 +169,13 @@ let _ =
Printexc.record_backtrace true;
Frontend.init ();
parse_cmdline cmdline_actions;
- if !option_o <> None && !num_input_files >= 2 then begin
- eprintf "Ambiguous '-o' option (multiple source files)\n";
- exit 2
- end;
- if !num_input_files = 0 then begin
- eprintf "clightgen: error: no input file\n";
- exit 2
- end;
+ if !option_o <> None && !num_input_files >= 2 then
+ fatal_error no_loc "Ambiguous '-o' option (multiple source files)";
+ if !num_input_files = 0 then
+ fatal_error no_loc "no input file";
perform_actions ()
+ with
+ | Sys_error msg
+ | CmdError msg -> error no_loc "%s" msg; exit 2
+ | Abort -> exit 2
+ | e -> crash e
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 5baed5dc..7c4c8f8a 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -340,7 +340,7 @@ let pp_instructions pp ic =
begin match ef with
| EF_inline_asm _ ->
instruction pp "Pinlineasm" [Id];
- Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump"
+ Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump")
| EF_annot (kind,txt,targs) ->
let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in
let len = String.length annot_string in
generated by cgit (git 2.34.1) at 2024-05-20 10:59:26 +0000