diff options
Diffstat (limited to 'src/extraction/Extraction.v')
| -rw-r--r-- | src/extraction/Extraction.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 20fc48c..b65bc41 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -55,9 +55,13 @@ From compcert Require Parser Initializers. +From cohpred_theory Require + Smtpredicate. + (* Standard lib *) Require Import ExtrOcamlBasic. Require Import ExtrOcamlString. +Require Import ExtrOCamlInt63. (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". @@ -172,7 +176,7 @@ Extract Constant Cabs.char_code => "int64". Load extractionMachdep. (* Avoid name clashes *) -Extraction Blacklist List String Int. +Extraction Blacklist List String Int Uint63. (* Cutting the dependency to R. *) Extract Inlined Constant Defs.F2R => "fun _ -> assert false". @@ -185,6 +189,8 @@ Extract Constant GibleSeqgen.partition => "Partition.partition". Extract Constant GiblePargen.schedule => "Schedule.schedule_fn". Extract Constant Abstr.print_forest => "(PrintAbstr.print_forest stdout)". +Extract Constant Smtpredicate.pred_verit_unsat => "Cohpred.smt_certificate". + (* 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])".*) @@ -202,6 +208,8 @@ Separate Extraction Verilog.stmnt_to_list Bourdoncle.bourdoncle + Smtpredicate.check_smt_total + 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 |