diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 16:33:57 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-04-27 16:33:57 +0100 |
| commit | e2d7bba73f52285475da813433c703d7df7ae44a (patch) | |
| tree | 370ace815a967f1847103e4a26f7b94c81dc323d /src/extraction | |
| parent | 405e822a4e769969ef01a683d486accee0d71da2 (diff) | |
| download | vericert-e2d7bba73f52285475da813433c703d7df7ae44a.tar.gz vericert-e2d7bba73f52285475da813433c703d7df7ae44a.zip | |
Update to Coq 8.17 and CompCert 3.12
Diffstat (limited to 'src/extraction')
| -rw-r--r-- | src/extraction/Extraction.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index aba2fe7..6357531 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -178,7 +178,6 @@ Extraction Blacklist List String Int. Extract Inlined Constant Defs.F2R => "fun _ -> assert false". Extract Inlined Constant Binary.FF2R => "fun _ -> assert false". 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".*) @@ -187,7 +186,7 @@ Extract Constant GiblePargen.schedule => "Schedule.schedule_fn". (* Loop normalization *) Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". -Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])". +(*Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".*) (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -204,7 +203,8 @@ 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.build_composite_env + Ctypes.merge_attributes Ctypes.remove_attributes + Ctypes.build_composite_env Ctypes.layout_struct Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr Csyntax.Eselection Ctyping.typecheck_program @@ -216,6 +216,7 @@ Separate Extraction Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs Conventions1.dummy_int_reg Conventions1.dummy_float_reg + Conventions1.allocatable_registers RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg |