From befbc76f89f3d8abc8da17caf91ea4a87ec96eeb Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 28 Mar 2012 13:32:21 +0000 Subject: checklink: first import of Valentin Robert's validator for asm and link cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/Cerrors.ml | 55 ++++++++++++++++++++++++++++++++++++++++++++++++ cparser/Cerrors.mli | 22 +++++++++++++++++++ cparser/Cparser.mllib | 21 ++++++++++++++++++ cparser/Cutil.ml | 2 +- cparser/Elab.ml | 8 +++---- cparser/Errors.ml | 55 ------------------------------------------------ cparser/Errors.mli | 22 ------------------- cparser/PackedStructs.ml | 2 +- cparser/Parse.ml | 8 +++---- cparser/Parse_aux.ml | 2 +- cparser/Rename.ml | 4 ++-- cparser/Unblock.ml | 2 +- cparser/libCparser.clib | 1 + 13 files changed, 113 insertions(+), 91 deletions(-) create mode 100644 cparser/Cerrors.ml create mode 100644 cparser/Cerrors.mli create mode 100644 cparser/Cparser.mllib delete mode 100644 cparser/Errors.ml delete mode 100644 cparser/Errors.mli create mode 100644 cparser/libCparser.clib (limited to 'cparser') diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml new file mode 100644 index 0000000..188531e --- /dev/null +++ b/cparser/Cerrors.ml @@ -0,0 +1,55 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Management of errors and warnings *) + +open Format + +let warn_error = ref false + +let num_errors = ref 0 +let num_warnings = ref 0 + +let reset () = num_errors := 0; num_warnings := 0 + +exception Abort + +let fatal_error fmt = + incr num_errors; + kfprintf + (fun _ -> raise Abort) + err_formatter + ("@[" ^^ fmt ^^ ".@]@.@[Fatal error.@]@.") + +let error fmt = + incr num_errors; + eprintf ("@[" ^^ fmt ^^ ".@]@.") + +let warning fmt = + incr num_warnings; + eprintf ("@[" ^^ fmt ^^ ".@]@.") + +let check_errors () = + if !num_errors > 0 then + eprintf "@[%d error%s detected.@]@." + !num_errors + (if !num_errors = 1 then "" else "s"); + if !warn_error && !num_warnings > 0 then + eprintf "@[%d error-enabled warning%s detected.@]@." + !num_warnings + (if !num_warnings = 1 then "" else "s"); + !num_errors > 0 || (!warn_error && !num_warnings > 0) + + diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli new file mode 100644 index 0000000..557fb14 --- /dev/null +++ b/cparser/Cerrors.mli @@ -0,0 +1,22 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +val warn_error : bool ref +val reset : unit -> unit +exception Abort +val fatal_error : ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a +val error : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +val warning : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a +val check_errors : unit -> bool diff --git a/cparser/Cparser.mllib b/cparser/Cparser.mllib new file mode 100644 index 0000000..c5dc513 --- /dev/null +++ b/cparser/Cparser.mllib @@ -0,0 +1,21 @@ +Cerrors +Cabs +Cabshelper +Parse_aux +Parser +Lexer +Machine +Env +Cprint +Cutil +Ceval +Cleanup +Builtins +Elab +Rename +Transform +Unblock +StructReturn +Bitfields +PackedStructs +Parse diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index eb3f063..4856c01 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -16,7 +16,7 @@ (* Operations on C types and abstract syntax *) open Printf -open Errors +open Cerrors open C open Env open Machine diff --git a/cparser/Elab.ml b/cparser/Elab.ml index f9b70c4..2473cf2 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -16,7 +16,7 @@ (* Elaboration from Cabs parse tree to C simplified, typed syntax tree *) open Format -open Errors +open Cerrors open Machine open Cabs open Cabshelper @@ -29,13 +29,13 @@ open Env (* Error reporting *) let fatal_error loc fmt = - Errors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + Cerrors.fatal_error ("%a: Error:@ " ^^ fmt) format_cabsloc loc let error loc fmt = - Errors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc + Cerrors.error ("%a: Error:@ " ^^ fmt) format_cabsloc loc let warning loc fmt = - Errors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc + Cerrors.warning ("%a: Warning:@ " ^^ fmt) format_cabsloc loc (* Error reporting for Env functions *) diff --git a/cparser/Errors.ml b/cparser/Errors.ml deleted file mode 100644 index 188531e..0000000 --- a/cparser/Errors.ml +++ /dev/null @@ -1,55 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Management of errors and warnings *) - -open Format - -let warn_error = ref false - -let num_errors = ref 0 -let num_warnings = ref 0 - -let reset () = num_errors := 0; num_warnings := 0 - -exception Abort - -let fatal_error fmt = - incr num_errors; - kfprintf - (fun _ -> raise Abort) - err_formatter - ("@[" ^^ fmt ^^ ".@]@.@[Fatal error.@]@.") - -let error fmt = - incr num_errors; - eprintf ("@[" ^^ fmt ^^ ".@]@.") - -let warning fmt = - incr num_warnings; - eprintf ("@[" ^^ fmt ^^ ".@]@.") - -let check_errors () = - if !num_errors > 0 then - eprintf "@[%d error%s detected.@]@." - !num_errors - (if !num_errors = 1 then "" else "s"); - if !warn_error && !num_warnings > 0 then - eprintf "@[%d error-enabled warning%s detected.@]@." - !num_warnings - (if !num_warnings = 1 then "" else "s"); - !num_errors > 0 || (!warn_error && !num_warnings > 0) - - diff --git a/cparser/Errors.mli b/cparser/Errors.mli deleted file mode 100644 index 557fb14..0000000 --- a/cparser/Errors.mli +++ /dev/null @@ -1,22 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -val warn_error : bool ref -val reset : unit -> unit -exception Abort -val fatal_error : ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a -val error : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -val warning : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a -val check_errors : unit -> bool diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index f926ece..0dbc7cb 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -20,7 +20,7 @@ open Machine open C open Cutil open Env -open Errors +open Cerrors open Transform type field_info = { diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 0fc85bf..2a144e2 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -39,15 +39,15 @@ let parse_transformations s = !t let preprocessed_file transfs name sourcefile = - Errors.reset(); + Cerrors.reset(); let t = parse_transformations transfs in let ic = open_in sourcefile in let p = try transform_program t (Elab.elab_preprocessed_file name ic) with Parsing.Parse_error -> - Errors.error "Error during parsing"; [] - | Errors.Abort -> + Cerrors.error "Error during parsing"; [] + | Cerrors.Abort -> [] in close_in ic; - if Errors.check_errors() then None else Some p + if Cerrors.check_errors() then None else Some p diff --git a/cparser/Parse_aux.ml b/cparser/Parse_aux.ml index 6592245..0600261 100755 --- a/cparser/Parse_aux.ml +++ b/cparser/Parse_aux.ml @@ -14,7 +14,7 @@ (* *********************************************************************) open Format -open Errors +open Cerrors open Cabshelper (* Report parsing errors *) diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 76c3c12..034df24 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -83,8 +83,8 @@ let ident env id = try IdentMap.find id env.re_id with Not_found -> - Errors.fatal_error "Internal error: Rename: %s__%d unbound" - id.name id.stamp + Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" + id.name id.stamp let rec typ env = function | TPtr(ty, a) -> TPtr(typ env ty, a) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index fa304b7..abdc5d5 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -20,7 +20,7 @@ open C open Cutil -open Errors +open Cerrors (* Convert an initializer to a list of assignments. Prepend those assignments to the given statement. *) diff --git a/cparser/libCparser.clib b/cparser/libCparser.clib new file mode 100644 index 0000000..1b55150 --- /dev/null +++ b/cparser/libCparser.clib @@ -0,0 +1 @@ +cparser/uint64.o -- cgit v1.2.3