diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-22 19:34:45 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-22 19:34:45 +0100 |
| commit | e89f1e606bc8c9c425628392adc9c69cec666b5e (patch) | |
| tree | 9c1d9bccb0811666a5f51c89a4285a4d747f34b7 /driver/Driver.ml | |
| parent | f1db887befa816f70f64aaffa2ce4d92c4bebc55 (diff) | |
| download | compcert-kvx-e89f1e606bc8c9c425628392adc9c69cec666b5e.tar.gz compcert-kvx-e89f1e606bc8c9c425628392adc9c69cec666b5e.zip | |
Represent struct and union types by name instead of by structure.
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index fec87420..f2a98f81 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -108,7 +108,7 @@ let parse_c_file sourcename ifile = end; (* Conversion to Csyntax *) let csyntax = - match C2C.convertProgram ast with + match Timing.time "CompCert C generation" C2C.convertProgram ast with | None -> exit 2 | Some p -> p in flush stderr; |