diff options
author | James Pollard <james@pollard.dev> | 2020-06-30 17:39:09 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-30 17:39:09 +0100 |
commit | a8aaca57d901e219d52ccae03833a59a75aaafe2 (patch) | |
tree | 6b56c0964663257e9cf06f989fa3bd6aaee9ea11 /driver/CoqupDriver.ml | |
parent | ffc978ec677f2f37ab8d8d1bf865cddadf087b81 (diff) | |
parent | f26f3887d0b0ac286c317a5425a3a4781871cfc2 (diff) | |
download | vericert-a8aaca57d901e219d52ccae03833a59a75aaafe2.tar.gz vericert-a8aaca57d901e219d52ccae03833a59a75aaafe2.zip |
Merge branch 'develop' of github.com:ymherklotz/coqup into develop
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 @ |