aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorJames Pollard <james@pollard.dev>2020-06-30 17:39:09 +0100
committerJames Pollard <james@pollard.dev>2020-06-30 17:39:09 +0100
commita8aaca57d901e219d52ccae03833a59a75aaafe2 (patch)
tree6b56c0964663257e9cf06f989fa3bd6aaee9ea11 /driver
parentffc978ec677f2f37ab8d8d1bf865cddadf087b81 (diff)
parentf26f3887d0b0ac286c317a5425a3a4781871cfc2 (diff)
downloadvericert-a8aaca57d901e219d52ccae03833a59a75aaafe2.tar.gz
vericert-a8aaca57d901e219d52ccae03833a59a75aaafe2.zip
Merge branch 'develop' of github.com:ymherklotz/coqup into develop
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 @