diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 12:34:35 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-30 12:34:35 +0100 |
commit | f26f3887d0b0ac286c317a5425a3a4781871cfc2 (patch) | |
tree | ef89abc630bcc6087b38aba18fd859311e2d3ed1 /driver/CoqupDriver.ml | |
parent | ae3f6b6096ab2484c1b3dcfab7f3f72bcfd268d5 (diff) | |
download | vericert-f26f3887d0b0ac286c317a5425a3a4781871cfc2.tar.gz vericert-f26f3887d0b0ac286c317a5425a3a4781871cfc2.zip |
Add command line flags for initial block
Diffstat (limited to 'driver/CoqupDriver.ml')
-rw-r--r-- | driver/CoqupDriver.ml | 8 |
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 @ |