diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Elab.ml | 7 | ||||
| -rw-r--r-- | cparser/Elab.mli | 2 | ||||
| -rw-r--r-- | cparser/Parse.ml | 16 |
3 files changed, 13 insertions, 12 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index e468ab2..0d2cb89 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2081,11 +2081,8 @@ let _ = elab_funbody_f := elab_funbody (** * Entry point *) -let elab_preprocessed_file name ic = - let lb = Lexer.init name ic in +let elab_file prog = reset(); - ignore (elab_definitions false (Builtins.environment()) - (Parser.file Lexer.initial lb)); - Lexer.finish(); + ignore (elab_definitions false (Builtins.environment()) prog); elaborated_program() diff --git a/cparser/Elab.mli b/cparser/Elab.mli index 007e3d4..7eee4a0 100644 --- a/cparser/Elab.mli +++ b/cparser/Elab.mli @@ -13,4 +13,4 @@ (* *) (* *********************************************************************) -val elab_preprocessed_file : string -> in_channel -> C.program +val elab_file : Cabs.definition list -> C.program diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 2a144e2..4a2ced2 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -40,14 +40,18 @@ let parse_transformations s = let preprocessed_file transfs name sourcefile = Cerrors.reset(); - let t = parse_transformations transfs in let ic = open_in sourcefile in let p = try - transform_program t (Elab.elab_preprocessed_file name ic) - with Parsing.Parse_error -> - Cerrors.error "Error during parsing"; [] - | Cerrors.Abort -> - [] in + let t = parse_transformations transfs in + let lb = Lexer.init name ic in + let parse = Clflags.time2 "Parsing" Parser.file Lexer.initial lb in + let p1 = Clflags.time "Elaboration" Elab.elab_file parse in + Clflags.time2 "Emulations" transform_program t p1 + with + | Parsing.Parse_error -> + Cerrors.error "Error during parsing"; [] + | Cerrors.Abort -> + [] in close_in ic; if Cerrors.check_errors() then None else Some p |