diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-12-09 20:06:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-12-09 20:06:34 +0000 |
| commit | b91f6db17ee30efd2068efbeecbf1d2b4c3850ea (patch) | |
| tree | 01dbe430a4d46d31e38cd6cf0774822b1f3416c4 /src/extraction | |
| parent | a64ccb64e16175b520a0dc4badde44a1cc46f17d (diff) | |
| download | vericert-b91f6db17ee30efd2068efbeecbf1d2b4c3850ea.tar.gz vericert-b91f6db17ee30efd2068efbeecbf1d2b4c3850ea.zip | |
Add bourdoncle to build
Diffstat (limited to 'src/extraction')
| -rw-r--r-- | src/extraction/Extraction.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 9b82e1b..395ec47 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -24,9 +24,10 @@ From vericert Require RTLPar RTLBlockInstr HTLgen - Pipeline + (*Pipeline*) HLSOpts Predicate + Bourdoncle . From Coq Require DecidableClass. @@ -182,10 +183,13 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false". Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". -Extract Constant Pipeline.pipeline => "pipelining.pipeline". +(*Extract Constant Pipeline.pipeline => "pipelining.pipeline".*) Extract Constant RTLBlockgen.partition => "Partition.partition". Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". +(* Loop normalization *) +Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". + (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -195,9 +199,9 @@ Separate Extraction vericert.Compiler.transf_hls_temp RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr - Pipeline.pipeline Predicate.sat_pred_simple Verilog.stmnt_to_list + Bourdoncle.bourdoncle Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state |