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/hls/GiblePargen.v | |
parent | 323f262727ac3a4b129bdaeaa21083d8daa5184c (diff) | |
download | vericert-4d262face34cb79d478823fd8db32cf02dc187f8.tar.gz vericert-4d262face34cb79d478823fd8db32cf02dc187f8.zip |
Add SMTCoq solver as dependency
Diffstat (limited to 'src/hls/GiblePargen.v')
-rw-r--r-- | src/hls/GiblePargen.v | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 736f461..25531a8 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -26,8 +26,11 @@ Require Import compcert.common.Values. Require Import compcert.lib.Floats. Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. +Require compcert.common.Errors. Require compcert.verilog.Op. +Module Err := compcert.common.Errors. + Require Import vericert.common.Vericertlib. Require Import vericert.common.Monad. Require Import vericert.hls.GibleSeq. @@ -464,19 +467,19 @@ Top-level Functions Parameter schedule : GibleSeq.function -> GiblePar.function. Definition transl_function (f: GibleSeq.function) - : Errors.res GiblePar.function := + : Err.res GiblePar.function := let tfcode := fn_code (schedule f) in if check_scheduled_trees f.(GibleSeq.fn_code) tfcode then - Errors.OK (mkfunction f.(GibleSeq.fn_sig) + Err.OK (mkfunction f.(GibleSeq.fn_sig) f.(GibleSeq.fn_params) f.(GibleSeq.fn_stacksize) tfcode f.(GibleSeq.fn_entrypoint)) else - Errors.Error - (Errors.msg "GiblePargen: Could not prove the blocks equivalent."). + Err.Error + (Err.msg "GiblePargen: Could not prove the blocks equivalent."). Definition transl_fundef := transf_partial_fundef transl_function. -Definition transl_program (p : GibleSeq.program) : Errors.res GiblePar.program := +Definition transl_program (p : GibleSeq.program) : Err.res GiblePar.program := transform_partial_program transl_fundef p. |