Commit 2a8888a2 authored by Joachim Bard's avatar Joachim Bard

added let-mapping for inlining

parent 8a65a53f
......@@ -17,7 +17,7 @@ Definition RangeValidator e A P Qmap dVars :=
then true
else match validAffineBounds e A P dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => validSMTIntervalbounds e A P Qmap dVars
| None => validSMTIntervalbounds e A P Qmap (fun _ => None) dVars
end.
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond)
......@@ -66,7 +66,7 @@ Definition RangeValidatorCmd e A P Qmap dVars:=
then true
else match validAffineBoundsCmd e A P dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => validSMTIntervalboundsCmd e A P Qmap dVars
| None => validSMTIntervalboundsCmd e A P Qmap (fun _ => None) dVars
end.
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond)
......
......@@ -702,7 +702,7 @@ Proof.
inversion H1; subst.
destruct m1; try discriminate.
now constructor.
Admitted.
Abort.
Lemma test_RangeBound_let_low_sound E P preQ m x e e1 e2 r Gamma v :
eval_precond E P
......@@ -715,8 +715,8 @@ Proof.
intros validP chk unsatQ Heq H.
eapply RangeBound_low_sound; eauto.
rewrite Heq.
eapply test_let_to_expr; eauto.
Qed.
(* eapply test_let_to_expr; eauto. *)
Abort.
Lemma test_RangeBound_cmd_low_sound E P preQ e f r Gamma v :
eval_precond E P
......@@ -726,4 +726,4 @@ Lemma test_RangeBound_cmd_low_sound E P preQ e f r Gamma v :
-> bstep (toREvalCmd (toRCmd f)) E (toRTMap Gamma) DeltaMapR v REAL
-> Q2R r <= v.
Proof.
Admitted.
Abort.
This diff is collapsed.
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