1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Entry point for the library: parse, elaborate, and transform *)
18 module CharSet = Set.Make(struct type t = char let compare = compare end)
20 let transform_program t p =
21 let run_pass pass flag p = if CharSet.mem flag t then pass p else p in
23 (run_pass (AddCasts.program ~all:(CharSet.mem 'C' t)) 'c'
24 (run_pass StructAssign.program 'S'
25 (run_pass StructByValue.program 's'
26 (run_pass Bitfields.program 'f'
27 (run_pass (SimplExpr.program ~volatile:(CharSet.mem 'v' t)) 'e'
28 (run_pass Unblock.program 'b'
31 let parse_transformations s =
32 let t = ref CharSet.empty in
33 let set s = String.iter (fun c -> t := CharSet.add c !t) s in
35 (function 'b' -> set "b"
47 let preprocessed_file transfs name lb =
49 let t = parse_transformations transfs in
52 Rename.program (transform_program t (Elab.elab_preprocessed_file lb))
53 with Parsing.Parse_error ->
54 Errors.error "Error during parsing"; []
57 if Errors.check_errors() then None else Some p