aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-06-12 12:04:12 +0100
committerYann Herklotz <git@yannherklotz.com>2020-06-12 12:04:12 +0100
commit1ae7c94199862f48eaf37f2f66f130bde215b9e0 (patch)
treed2a89cf988c184a2fd8138ec7c3fb0c8a6cc0033 /driver
parentc358d4a8fc6073b24c3f270d0525644b03a4f291 (diff)
downloadvericert-1ae7c94199862f48eaf37f2f66f130bde215b9e0.tar.gz
vericert-1ae7c94199862f48eaf37f2f66f130bde215b9e0.zip
Fix main function
Diffstat (limited to 'driver')
-rw-r--r--driver/CoqupDriver.ml20
1 files changed, 3 insertions, 17 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 8363ca5..3dd0ed1 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -27,7 +27,6 @@
*)
open Printf
-open Coqup.Camlcoq
open Coqup.Commandline
open Coqup.Clflags
open Coqup.CommonOptions
@@ -100,22 +99,9 @@ let compile_c_file sourcename ifile ofile =
| Coqup.Errors.Error msg ->
let loc = file_loc sourcename in
fatal_error loc "%a" print_error msg in
- if not !option_simulate then begin
- let oc = open_out ofile in
- Coqup.PrintVerilog.print_program oc verilog;
- close_out oc
- end else begin
- 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
- Coqup.PrintVerilog.print_result stdout state;
- print_string "Result: ";
- Coqup.PrintVerilog.print_value stdout result;
- print_newline ()
- end
+ let oc = open_out ofile in
+ Coqup.PrintVerilog.print_program oc verilog;
+ close_out oc
end
(* From C source to asm *)