From b184e05aada74f34dafd9d1bf6bc24e68ab76e05 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sun, 7 Aug 2016 14:57:22 +0200 Subject: Exit earlier on wrong return types. Return with a expression that is not compatible with the given return type of a function now causes and fatal error, to avoid problems with later transformation passes depending on it. --- cparser/Elab.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 76f8efdb..67b23d91 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2361,7 +2361,7 @@ let rec elab_stmt env ctx s = instead of the expected type@ %a" Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ else - error loc + fatal_error loc "return value has type@ %a@ \ instead of the expected type@ %a" Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ -- cgit From 8228d4f959c2211d1840928d1cfc349ce2820200 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 8 Aug 2016 10:37:53 +0200 Subject: Added error check before transformations. Added a check for errors after the elab phases to avoid problems in the transformations due to broken input programs. Bug 19504 --- cparser/Cerrors.ml | 6 ++++-- cparser/Cerrors.mli | 1 + cparser/Elab.ml | 2 +- cparser/Parse.ml | 1 + 4 files changed, 7 insertions(+), 3 deletions(-) (limited to 'cparser') diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 5c077f37..0667ea16 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -30,7 +30,7 @@ exception Abort to print its message, as opposed to [Format], and does not automatically introduce indentation and a final dot into the message. This is useful for multi-line messages. *) - + let fatal_error_raw fmt = incr num_errors; Printf.kfprintf @@ -67,4 +67,6 @@ let check_errors () = (if !num_warnings = 1 then "" else "s"); !num_errors > 0 || (!warn_error && !num_warnings > 0) - +let raise_on_errors () = + if !num_warnings > 0 || (!warn_error && !num_warnings > 0) then + raise Abort diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index 3e315fad..313573c3 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -22,3 +22,4 @@ val error : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val warning : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val info : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val check_errors : unit -> bool +val raise_on_errors : unit -> unit diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 67b23d91..76f8efdb 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2361,7 +2361,7 @@ let rec elab_stmt env ctx s = instead of the expected type@ %a" Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ else - fatal_error loc + error loc "return value has type@ %a@ \ instead of the expected type@ %a" Cprint.typ b.etyp Cprint.typ ctx.ctx_return_typ diff --git a/cparser/Parse.ml b/cparser/Parse.ml index c125e653..3f60ebb4 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -74,6 +74,7 @@ let preprocessed_file transfs name sourcefile = | 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 -> -- cgit From 6c70ceb179798478f29efda5358c4660c38b7392 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 8 Aug 2016 12:50:44 +0200 Subject: Fixed typo. Bug 19504 --- cparser/Cerrors.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 0667ea16..a4d1a3f8 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -68,5 +68,5 @@ let check_errors () = !num_errors > 0 || (!warn_error && !num_warnings > 0) let raise_on_errors () = - if !num_warnings > 0 || (!warn_error && !num_warnings > 0) then + if !num_errors > 0 || (!warn_error && !num_warnings > 0) then raise Abort -- cgit From b1a059251053a061d98e4b440bfab40ffd8761c7 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 17 Aug 2016 11:05:56 +0200 Subject: Catch attribute excpetion in _Alignas elab The exception Wrong_attr_arg raised is now catched during the translation of the wrong _Alignas attributes. Bug 19568. --- cparser/Elab.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 76f8efdb..1586f142 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -433,6 +433,7 @@ let elab_attribute env = function begin match elab_attr_arg loc env a with | AInt n when is_power_of_two n -> [AAlignas (Int64.to_int n)] | _ -> warning loc "bad _Alignas value, ignored"; [] + | exception Wrong_attr_arg -> warning loc "bad _Alignas value, ignored"; [] end | ALIGNAS_ATTR (_, loc) -> warning loc "_Alignas takes exactly one parameter, ignored"; [] -- cgit From e2b4459ccd1b0f8436cb70a631772d715e642dcd Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 17 Aug 2016 12:34:28 +0200 Subject: Exit earlier on empty union. Instead of a warning for an empty union CompCert reports an error and exits. This avoids problems during the generation of initializers for these. Bug 19565. --- cparser/Elab.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'cparser') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 1586f142..8cd7ed64 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -813,7 +813,11 @@ and elab_struct_or_union_info kind loc env members attrs = check_incomplete m; (* Warn for empty structs or unions *) if m = [] then - warning loc "empty %s" (if kind = Struct then "struct" else "union"); + if kind = Struct then begin + warning loc "empty struct" + end else begin + fatal_error loc "empty union" + end; (composite_info_def env' kind attrs m, env') and elab_struct_or_union only kind loc tag optmembers attrs env = -- cgit