aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cerrors.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-08-08 10:37:53 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-08-08 10:37:53 +0200
commit8228d4f959c2211d1840928d1cfc349ce2820200 (patch)
tree01e9da05ca158ea53b447c67983058a25eb88d0d /cparser/Cerrors.ml
parentb184e05aada74f34dafd9d1bf6bc24e68ab76e05 (diff)
downloadcompcert-8228d4f959c2211d1840928d1cfc349ce2820200.tar.gz
compcert-8228d4f959c2211d1840928d1cfc349ce2820200.zip
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
Diffstat (limited to 'cparser/Cerrors.ml')
-rw-r--r--cparser/Cerrors.ml6
1 files changed, 4 insertions, 2 deletions
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