aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-04-22 00:13:14 +0100
committerYann Herklotz <git@yannherklotz.com>2020-04-22 00:13:14 +0100
commitf7782d10e4dbecab7c043f8409772d6e2b0eb7d6 (patch)
tree00a7d32b74005421684d610132999477beb43ff5 /driver
parentb9785cabf40b9b7708f1c0d5a622d7fc4713c38d (diff)
downloadvericert-f7782d10e4dbecab7c043f8409772d6e2b0eb7d6.tar.gz
vericert-f7782d10e4dbecab7c043f8409772d6e2b0eb7d6.zip
Improve the printing of results
Diffstat (limited to 'driver')
-rw-r--r--driver/CoqupDriver.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 80b4145..8363ca5 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -105,15 +105,16 @@ let compile_c_file sourcename ifile ofile =
Coqup.PrintVerilog.print_program oc verilog;
close_out oc
end else begin
- print_endline "Simulating";
- let result =
+ let result, state =
match Coqup.Simulator.simulate (Nat.of_int 100) verilog with
| Coqup.Errors.OK r -> r
| Coqup.Errors.Error msg ->
let loc = file_loc sourcename in
fatal_error loc "%a" print_error msg in
- printf "Length: %d\n" (List.length result);
- Coqup.PrintVerilog.print_result result
+ Coqup.PrintVerilog.print_result stdout state;
+ print_string "Result: ";
+ Coqup.PrintVerilog.print_value stdout result;
+ print_newline ()
end
end