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 /extraction | |
| 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 'extraction')
| -rw-r--r-- | extraction/extraction.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index ee496ffa..0ba4abdd 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -23,6 +23,8 @@ Require ValueDomain. Require Tailcall. Require Allocation. Require Ctypes. +Require Csyntax. +Require Clight. Require Compiler. Require Parser. Require Initializers. @@ -157,7 +159,8 @@ Cd "extraction". Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state - Ctypes.merge_attributes Ctypes.remove_attributes + Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env + Csyntax.make_program Clight.make_program Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr Conventions1.dummy_int_reg Conventions1.dummy_float_reg |