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/SelectOpproof.v | |
| parent | 9c2c662a2a70545858d95b2f9f0a3625c506bc24 (diff) | |
| download | compcert-kvx-cdb48111d4baff50d8708b979f8b31ef21505247.tar.gz compcert-kvx-cdb48111d4baff50d8708b979f8b31ef21505247.zip | |
risc-V now without trapping instructions
Diffstat (limited to 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 436cd4f3..1d13702a 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -788,6 +788,7 @@ Theorem eval_intoffloat: exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold intoffloat. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_intuoffloat: @@ -797,6 +798,7 @@ Theorem eval_intuoffloat: exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold intuoffloat. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_floatofintu: @@ -808,6 +810,7 @@ Proof. intros until y; unfold floatofintu. case (floatofintu_match a); intros. InvEval. simpl in H0. TrivialExists. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_floatofint: @@ -819,6 +822,7 @@ Proof. intros until y; unfold floatofint. case (floatofint_match a); intros. InvEval. simpl in H0. TrivialExists. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_intofsingle: @@ -828,6 +832,7 @@ Theorem eval_intofsingle: exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold intofsingle. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleofint: @@ -837,6 +842,7 @@ Theorem eval_singleofint: exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v. Proof. intros; unfold singleofint; TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_intuofsingle: @@ -846,6 +852,7 @@ Theorem eval_intuofsingle: exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold intuofsingle. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleofintu: @@ -855,6 +862,7 @@ Theorem eval_singleofintu: exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v. Proof. intros; unfold intuofsingle. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. |