Add project files and compcert interconnect

2 files changed, 19 insertions, 0 deletions

diff --git a/extraction/driver.ml b/extraction/driver.ml
new file mode 100644
index 0000000..f14a876
--- /dev/null
+++ b/extraction/driver.ml
@@ -0,0 +1,19 @@
+(* 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
+ *)
+open Compcert.Allocation
+
+let _ = print_endline "Hello world"
diff --git a/extraction/driver.mli b/extraction/driver.mli
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/extraction/driver.mli