diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 22:58:34 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 22:58:34 +0200 |
commit | 68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0 (patch) | |
tree | aebe9f1dc7d8e0e0152c0c8f082b6395b91e93da /mppa_k1c/Op.v | |
parent | 6064bac57701ba0a12031d43acbe25cb0140730c (diff) | |
download | compcert-kvx-68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0.tar.gz compcert-kvx-68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0.zip |
osel imm
Diffstat (limited to 'mppa_k1c/Op.v')
-rw-r--r-- | mppa_k1c/Op.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 1b3a839f..35fbb596 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -456,8 +456,8 @@ Definition eval_operation | (Oinsf stop start), v0::v1::nil => Some (insf stop start v0 v1) | (Oinsfl stop start), v0::v1::nil => Some (insfl stop start v0 v1) | Osel c ty, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 v2 ty) - | Oselimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint) - | Osellimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong) + | Oselimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint) + | Osellimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong) | _, _ => None end. @@ -662,8 +662,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oinsf _ _ => (Tint :: Tint :: nil, Tint) | Oinsfl _ _ => (Tlong :: Tlong :: nil, Tlong) | Osel c ty => (ty :: ty :: arg_type_of_condition0 c :: nil, ty) - | Oselimm c ty => (Tint :: Tint :: arg_type_of_condition0 c :: nil, Tint) - | Osellimm c ty => (Tlong :: Tlong :: arg_type_of_condition0 c :: nil, Tlong) + | Oselimm c ty => (Tint :: arg_type_of_condition0 c :: nil, Tint) + | Osellimm c ty => (Tlong :: arg_type_of_condition0 c :: nil, Tlong) end. (* FIXME: two Tptr ?! *) @@ -1614,7 +1614,7 @@ Proof. (* Oselimm *) - apply Val.select_inject; trivial. - destruct (eval_condition0 c0 v2 m1) eqn:Hcond. + destruct (eval_condition0 _ _ _) eqn:Hcond. + right. symmetry. eapply eval_condition0_inj; eassumption. @@ -1622,7 +1622,7 @@ Proof. (* Osellimm *) - apply Val.select_inject; trivial. - destruct (eval_condition0 c0 v2 m1) eqn:Hcond. + destruct (eval_condition0 _ _ _) eqn:Hcond. + right. symmetry. eapply eval_condition0_inj; eassumption. |