diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-21 18:57:33 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-21 18:57:33 +0100 |
| commit | 4d262face34cb79d478823fd8db32cf02dc187f8 (patch) | |
| tree | 820335def3dc6d2fda3b779e8079b0c5fac8620c /src/extraction | |
| parent | 323f262727ac3a4b129bdaeaa21083d8daa5184c (diff) | |
| download | vericert-4d262face34cb79d478823fd8db32cf02dc187f8.tar.gz vericert-4d262face34cb79d478823fd8db32cf02dc187f8.zip | |
Add SMTCoq solver as dependency
Diffstat (limited to 'src/extraction')
| -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 |