diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 22:48:45 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 22:48:45 +0200 |
| commit | cdb48111d4baff50d8708b979f8b31ef21505247 (patch) | |
| tree | cf989a9b938f1d4c3d9fde26d568157790bc516f /riscV/SelectLongproof.v | |
| parent | 9c2c662a2a70545858d95b2f9f0a3625c506bc24 (diff) | |
| download | compcert-kvx-cdb48111d4baff50d8708b979f8b31ef21505247.tar.gz compcert-kvx-cdb48111d4baff50d8708b979f8b31ef21505247.zip | |
risc-V now without trapping instructions
Diffstat (limited to 'riscV/SelectLongproof.v')
| -rw-r--r-- | riscV/SelectLongproof.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index f5e8edf8..0fc578bf 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -558,6 +558,7 @@ Proof. unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longoffloat; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat. @@ -565,6 +566,7 @@ Proof. unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longuoffloat; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong. @@ -572,6 +574,7 @@ Proof. unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_floatoflong; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu. @@ -579,6 +582,7 @@ Proof. unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_floatoflongu; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. @@ -586,6 +590,7 @@ Proof. unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longofsingle; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle. @@ -593,6 +598,7 @@ Proof. unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longuofsingle; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. @@ -600,6 +606,7 @@ Proof. unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_singleoflong; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. @@ -607,6 +614,7 @@ Proof. unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_singleoflongu; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. End CMCONSTR. |