diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/driver.ml | 19 | ||||
| -rw-r--r-- | extraction/driver.mli | 0 |
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 |