diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 10:10:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 10:10:06 +0200 |
| commit | cfc681ae18c59f4a19143a7245be23eb6a4045a0 (patch) | |
| tree | 9de825a02fe2abd027cad7cb142c1220b7c5035f /mppa_k1c/Op.v | |
| parent | c0984982ea5b8481bfc75c0ea4254eb5db07d875 (diff) | |
| download | compcert-kvx-cfc681ae18c59f4a19143a7245be23eb6a4045a0.tar.gz compcert-kvx-cfc681ae18c59f4a19143a7245be23eb6a4045a0.zip | |
add finvw ; not yet generated
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 4beef520..de372157 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -189,6 +189,7 @@ Inductive operation : Type := | Odivfs (**r [rd = r1 / r2] *) | Ominfs | Omaxfs + | Oinvfs | Osingleoffloat (**r [rd] is [r1] truncated to single-precision float *) | Ofloatofsingle (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) @@ -440,6 +441,7 @@ Definition eval_operation | Odivfs, v1::v2::nil => Some (Val.divfs v1 v2) | Ominfs, v1::v2::nil => Some (ExtValues.minfs v1 v2) | Omaxfs, v1::v2::nil => Some (ExtValues.maxfs v1 v2) + | Oinvfs, v1::nil => Some (ExtValues.invfs v1) | Osingleoffloat, v1::nil => Some (Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 @@ -652,6 +654,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Odivfs | Ominfs | Omaxfs => (Tsingle :: Tsingle :: nil, Tsingle) + | Oinvfs => (Tsingle :: nil, Tsingle) | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) @@ -933,6 +936,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* minfs, maxfs *) - destruct v0; destruct v1... - destruct v0; destruct v1... + (* invfs *) + - destruct v0... (* singleoffloat, floatofsingle *) - destruct v0... - destruct v0... @@ -1550,6 +1555,8 @@ Proof. (* minfs, maxfs *) - inv H4; inv H2; simpl; auto. - inv H4; inv H2; simpl; auto. + (* invfs *) + - inv H4; simpl; auto. (* singleoffloat, floatofsingle *) - inv H4; simpl; auto. - inv H4; simpl; auto. |