diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 19:56:30 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 19:56:30 +0100 |
| commit | 59413cb4018d09fb3b641a49ab062bc933d5274c (patch) | |
| tree | 5599db40a806497089df856604d5917ea5549ea1 /extraction | |
| parent | 76c887ad132aa7b0c7ac72dca5d56e4c2bf1747a (diff) | |
| download | compcert-kvx-59413cb4018d09fb3b641a49ab062bc933d5274c.tar.gz compcert-kvx-59413cb4018d09fb3b641a49ab062bc933d5274c.zip | |
starts compiling but still fake
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index ea30e7c2..61c7c746 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -36,7 +36,8 @@ Require Parser. Require Initializers. Require Asmaux. -Require CSE3analysis. (* FIXME *) +Require CSE3. +Require CSE3analysis. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -115,6 +116,8 @@ Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". Extract Constant Compopts.optim_CSE2 => "fun _ -> !Clflags.option_fcse2". +Extract Constant Compopts.optim_CSE3 => + "fun _ -> !Clflags.option_fcse3". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => @@ -162,6 +165,8 @@ Extract Constant Cabs.loc => Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". +Extract Inlined Constant CSE3.preanalysis => "CSE3analysisaux.preanalysis". + Extract Inductive HashedSet.PSet_internals.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". Extract Inlined Constant HashedSet.PSet_internals.pset_eq => "(==)" (* "HashedSetaux.eq" *). @@ -188,7 +193,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - CSE3analysis.totoro (* FIXME *) + CSE3analysis.internal_analysis CSE3.run 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.build_composite_env |