1 files changed, 60 insertions, 6 deletions
diff --git a/extraction/driver.ml b/extraction/driver.ml
index f14a876..eb14d45 100644
--- a/extraction/driver.ml
+++ b/extraction/driver.ml
@@ -1,10 +1,12 @@
-(* let parse_c_file sourcename ifile =
+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 "")
+    ^ (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
@@ -13,7 +15,59 @@
   (* Save CompCert C AST if requested *)
   PrintCsyntax.print_if csyntax;
   csyntax
- *)
-open Compcert.Allocation
+
+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"