Commit 69ba85c7 authored by Heiko Becker's avatar Heiko Becker

Add a simple regression test for fixed-point checking

parent 124cb845
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const (F 32 22) ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition Rete3 := Ret e3.
Definition defVars_additionSimple :(nat -> option mType) := fun n =>
if n =? 0 then Some (F 32 24) else None.
Definition thePrecondition_additionSimple:precond := fun (n:nat) =>
if n =? 0 then ( (-100)#(1), (100)#(1)) else (0#1,0#1).
Definition absenv_additionSimple :analysisResult := Eval compute in
FloverMap.add e3 (( (1157)#(5), (2157)#(5)), (9)#(16777216)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (1)#(16777216)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1)#(4194304)) (FloverMap.empty (intv * error)))).
Theorem ErrorBound_additionSimple_Sound :
CertificateCheckerCmd Rete3 absenv_additionSimple thePrecondition_additionSimple defVars_additionSimple = true.
Proof.
vm_compute; auto.
Qed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment