aboutsummaryrefslogtreecommitdiffstats
path: root/driver/VericertDriver.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/VericertDriver.ml')
-rw-r--r--driver/VericertDriver.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index d45587c..ac358fe 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -99,8 +99,9 @@ let compile_c_file sourcename ifile ofile =
in
match translation csyntax with
| Vericert.Errors.OK v ->
- v
+ if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n"; v
| Vericert.Errors.Error msg ->
+ if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n";
let loc = file_loc sourcename in
fatal_error loc "%a" print_error msg in
let oc = open_out ofile in