aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-06-30 12:34:35 +0100
committerYann Herklotz <git@yannherklotz.com>2020-06-30 12:34:35 +0100
commitf26f3887d0b0ac286c317a5425a3a4781871cfc2 (patch)
treeef89abc630bcc6087b38aba18fd859311e2d3ed1 /driver
parentae3f6b6096ab2484c1b3dcfab7f3f72bcfd268d5 (diff)
downloadvericert-f26f3887d0b0ac286c317a5425a3a4781871cfc2.tar.gz
vericert-f26f3887d0b0ac286c317a5425a3a4781871cfc2.zip
Add command line flags for initial block
Diffstat (limited to 'driver')
-rw-r--r--driver/CoqupDriver.ml8
1 files changed, 3 insertions, 5 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 2932a50..afbe4d0 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -36,11 +36,7 @@ open Coqup.Frontend
open Coqup.Assembler
open Coqup.Linker
open Coqup.Diagnostics
-
-(* Coqup flags *)
-let option_simulate = ref false
-let option_hls = ref true
-let option_debug_hls = ref false
+open Coqup.CoqupClflags
(* Name used for version string etc. *)
let tool_name = "C verified high-level synthesis"
@@ -215,6 +211,7 @@ Processing options:
--no-hls Do not use HLS and generate standard flow.
--simulate Simulate the result with the Verilog semantics.
--debug-hls Add debug logic to the Verilog.
+ --initialise-stack initialise the stack to all 0s.
|} ^
prepro_help ^
language_support_help ^
@@ -316,6 +313,7 @@ let cmdline_actions =
[Exact "--no-hls", Unset option_hls;
Exact "--simulate", Set option_simulate;
Exact "--debug-hls", Set option_debug_hls;
+ Exact "--initialise-stack", Set option_initial;
]
(* Getting version info *)
@ version_options tool_name @