aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/ValueAOp.v
diff options
context:
space:
mode:
authorJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-04 03:04:21 +0100
committerJacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>2015-11-04 03:04:21 +0100
commit5664fddcab15ef4482d583673c75e07bd1e96d0a (patch)
tree878b22860e69405ba5cf6fd2798731dac8ce660c /powerpc/ValueAOp.v
parentb960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff)
parentfe73ed58ef80da7c53c124302a608948fb190229 (diff)
downloadcompcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz
compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip
Merge remote-tracking branch 'origin/master' into parser_fix
Diffstat (limited to 'powerpc/ValueAOp.v')
-rw-r--r--powerpc/ValueAOp.v9
1 files changed, 6 insertions, 3 deletions
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 8cb29145..fe5a0792 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -102,6 +102,9 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Osingleoffloat, v1::nil => singleoffloat v1
| Ofloatofsingle, v1::nil => floatofsingle v1
| Ointoffloat, v1::nil => intoffloat v1
+ | Ointuoffloat, v1::nil => intuoffloat v1
+ | Ofloatofint, v1::nil => floatofint v1
+ | Ofloatofintu, v1::nil => floatofintu v1
| Ofloatofwords, v1::v2::nil => floatofwords v1 v2
| Omakelong, v1::v2::nil => longofwords v1 v2
| Olowlong, v1::nil => loword v1
@@ -159,7 +162,7 @@ Theorem eval_static_addressing_sound:
Proof.
unfold eval_addressing, eval_static_addressing; intros;
destruct addr; InvHyps; eauto with va.
- rewrite Int.add_zero_l; auto with va.
+ rewrite Int.add_zero_l; auto with va.
Qed.
Theorem eval_static_operation_sound:
@@ -174,8 +177,8 @@ Proof.
destruct (propagate_float_constants tt); constructor.
rewrite Int.add_zero_l; eauto with va.
fold (Val.sub (Vint i) a1). auto with va.
- apply floatofwords_sound; auto.
- apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+ apply floatofwords_sound; auto.
+ apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
Qed.
End SOUNDNESS.