diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-04-02 14:54:14 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-04-02 14:54:20 +0100 |
commit | 8659e1b672a9b28a78c5b026312e7f3c0cb87c36 (patch) | |
tree | 7208310bcfa2cbae6dc8d244ee3693718df4a20b /driver/CoqupDriver.ml | |
parent | 5398b08ec6d445f91ed74c8434150cfbf99cc373 (diff) | |
download | vericert-8659e1b672a9b28a78c5b026312e7f3c0cb87c36.tar.gz vericert-8659e1b672a9b28a78c5b026312e7f3c0cb87c36.zip |
Handle loops and conditionals correctly
Diffstat (limited to 'driver/CoqupDriver.ml')
-rw-r--r-- | driver/CoqupDriver.ml | 4 |
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);] |