aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Parse.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:22:27 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:22:27 +0000
commit891377ce1962cdb31357d6580d6546ec22df2b4f (patch)
tree4ff7c38749cc7a4c1af411c5aa3eb7225c4ae6a1 /cparser/Parse.ml
parent018edf2d81bf94197892cf1df221f7eeac1f96f6 (diff)
downloadcompcert-kvx-891377ce1962cdb31357d6580d6546ec22df2b4f.tar.gz
compcert-kvx-891377ce1962cdb31357d6580d6546ec22df2b4f.zip
Switching to the new C parser/elaborator/simplifier
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/Parse.ml')
-rw-r--r--cparser/Parse.ml59
1 files changed, 59 insertions, 0 deletions
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
new file mode 100644
index 00000000..7dcc8d1d
--- /dev/null
+++ b/cparser/Parse.ml
@@ -0,0 +1,59 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(* Entry point for the library: parse, elaborate, and transform *)
+
+module CharSet = Set.Make(struct type t = char let compare = compare end)
+
+let transform_program t p =
+ let run_pass pass flag p = if CharSet.mem flag t then pass p else p in
+ Rename.program
+ (run_pass (AddCasts.program ~all:(CharSet.mem 'C' t)) 'c'
+ (run_pass StructAssign.program 'S'
+ (run_pass StructByValue.program 's'
+ (run_pass Bitfields.program 'f'
+ (run_pass (SimplExpr.program ~volatile:(CharSet.mem 'v' t)) 'e'
+ (run_pass Unblock.program 'b'
+ p))))))
+
+let parse_transformations s =
+ let t = ref CharSet.empty in
+ let set s = String.iter (fun c -> t := CharSet.add c !t) s in
+ String.iter
+ (function 'b' -> set "b"
+ | 'e' -> set "e"
+ | 'c' -> set "ec"
+ | 'C' -> set "ecC"
+ | 's' -> set "s"
+ | 'S' -> set "esS"
+ | 'v' -> set "ev"
+ | 'f' -> set "bef"
+ | _ -> ())
+ s;
+ !t
+
+let preprocessed_file transfs name sourcefile =
+ Errors.reset();
+ let t = parse_transformations transfs in
+ let ic = open_in sourcefile in
+ let p =
+ try
+ Rename.program (transform_program t (Elab.elab_preprocessed_file name ic))
+ with Parsing.Parse_error ->
+ Errors.error "Error during parsing"; []
+ | Errors.Abort ->
+ [] in
+ close_in ic;
+ if Errors.check_errors() then None else Some p