Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 9 insertions, 5 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 879d752..913fb50 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -196,17 +196,21 @@ Remark loadind_label:
   forall base ofs ty dst k c,
   loadind base ofs ty dst k = OK c -> tail_nolabel k c.
 Proof.
-  unfold loadind; intros.
-  destruct ty; destruct (Int.eq (high_s ofs) Int.zero);
+  unfold loadind, accessind; intros.
+  destruct ty; try discriminate;
+  destruct (preg_of dst); try discriminate;
+  destruct (Int.eq (high_s ofs) Int.zero);
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
 Remark storeind_label:
   forall base ofs ty src k c,
-  storeind base src ofs ty k = OK c -> tail_nolabel k c.
+  storeind src base ofs ty k = OK c -> tail_nolabel k c.
 Proof.
-  unfold storeind; intros.
-  destruct ty; destruct (Int.eq (high_s ofs) Int.zero);
+  unfold storeind, accessind; intros.
+  destruct ty; try discriminate;
+  destruct (preg_of src); try discriminate;
+  destruct (Int.eq (high_s ofs) Int.zero);
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.