aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-04-02 14:54:14 +0100
committerYann Herklotz <git@yannherklotz.com>2020-04-02 14:54:20 +0100
commit8659e1b672a9b28a78c5b026312e7f3c0cb87c36 (patch)
tree7208310bcfa2cbae6dc8d244ee3693718df4a20b /driver
parent5398b08ec6d445f91ed74c8434150cfbf99cc373 (diff)
downloadvericert-8659e1b672a9b28a78c5b026312e7f3c0cb87c36.tar.gz
vericert-8659e1b672a9b28a78c5b026312e7f3c0cb87c36.zip
Handle loops and conditionals correctly
Diffstat (limited to 'driver')
-rw-r--r--driver/CoqupDriver.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 92553c9..0a4f84f 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -85,7 +85,7 @@ let compile_i_file sourcename preproname =
""
end else if !option_S then begin
compile_c_file sourcename preproname
- (output_filename ~final:true sourcename ".c" ".s");
+ (output_filename ~final:true sourcename ".c" ".v");
""
end else begin
let asmname =
@@ -294,7 +294,7 @@ let cmdline_actions =
(* Processing options *)
[ Exact "-c", Set option_c;
Exact "-E", Set option_E;
- Exact "-S", Set option_S;
+ Exact "--hls", Set option_S;
Exact "-o", String(fun s -> option_o := Some s);
Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
option_o := Some s);]