diff options
Diffstat (limited to 'extraction')
-rw-r--r-- | extraction/Extraction.v | 4 | ||||
-rw-r--r-- | extraction/driver.ml | 73 | ||||
-rw-r--r-- | extraction/dune | 8 |
3 files changed, 0 insertions, 85 deletions
diff --git a/extraction/Extraction.v b/extraction/Extraction.v deleted file mode 100644 index 4c5f034..0000000 --- a/extraction/Extraction.v +++ /dev/null @@ -1,4 +0,0 @@ -From CoqUp Require Import Verilog. - -Cd "extraction". -Separate Extraction Verilog.nat_to_value Verilog.value_to_nat. diff --git a/extraction/driver.ml b/extraction/driver.ml deleted file mode 100644 index eb14d45..0000000 --- a/extraction/driver.ml +++ /dev/null @@ -1,73 +0,0 @@ -open Compcert - -let parse_c_file sourcename ifile = - (* Simplification options *) - let simplifs = - "b" (* blocks: mandatory *) - ^ (if false then "s" else "") - ^ (if false then "f" else "") - ^ (if false then "p" else "") - in - (* Parsing and production of a simplified C AST *) - let ast = Parse.preprocessed_file simplifs sourcename ifile in - (* Conversion to Csyntax *) - let csyntax = Timing.time "CompCert C generation" C2C.convertProgram ast in - (* Save CompCert C AST if requested *) - PrintCsyntax.print_if csyntax; - csyntax - -let compile_c_file sourcename ifile ofile = - (* Parse the ast *) - let csyntax = parse_c_file sourcename ifile in - (* Convert to Asm *) - let rtl = - match Compiler.apply_partial - (CoqUp.transf_frontend csyntax) with - | Errors.OK rtl -> - rtl - | Errors.Error msg -> - let loc = file_loc sourcename in - fatal_error loc "%a" print_error msg in - (* Print Asm in text form *) - let oc = open_out ofile in - PrintAsm.print_program oc asm; - close_out oc - -let compile_i_file sourcename preproname = - if !option_interp then begin - Machine.config := Machine.compcert_interpreter !Machine.config; - let csyntax = parse_c_file sourcename preproname in - Interp.execute csyntax; - "" - end else if !option_S then begin - compile_c_file sourcename preproname - (output_filename ~final:true sourcename ".c" ".s"); - "" - end else begin - let asmname = - if !option_dasm - then output_filename sourcename ".c" ".s" - else tmp_file ".s" in - compile_c_file sourcename preproname asmname; - let objname = object_filename sourcename ".c" in - assemble asmname objname; - objname - end - -(* Processing of a .c file *) - -let process_c_file sourcename = - ensure_inputfile_exists sourcename; - if !option_E then begin - preprocess sourcename (output_filename_default "-"); - "" - end else begin - let preproname = if !option_dprepro then - output_filename sourcename ".c" ".i" - else - tmp_file ".i" in - preprocess sourcename preproname; - compile_i_file sourcename preproname - end - -let _ = print_endline "Hello world" diff --git a/extraction/dune b/extraction/dune deleted file mode 100644 index 12a6b8d..0000000 --- a/extraction/dune +++ /dev/null @@ -1,8 +0,0 @@ -(executables - (flags (:standard -warn-error -A)) - (names driver) - (libraries compcert)) - -(install - (section bin) - (files (driver.exe as coqup))) |