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, 4 insertions, 0 deletions

diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml
index 49c0774..2d3efe3 100644
--- a/powerpc/Unusedglob1.ml
+++ b/powerpc/Unusedglob1.ml
@@ -42,18 +42,22 @@ let referenced_instr = function
   | Pcmpwi(_, c)
   | Plbz(_, c, _)
   | Plfd(_, c, _)
+  | Plfd_a(_, c, _)
   | Plfs(_, c, _)
   | Plha(_, c, _)
   | Plhz(_, c, _)
   | Plwz(_, c, _)
+  | Plwz_a(_, c, _)
   | Pmulli(_, _, c)
   | Pori(_, _, c)
   | Poris(_, _, c)
   | Pstb(_, c, _)
   | Pstfd(_, c, _)
+  | Pstfd_a(_, c, _)
   | Pstfs(_, c, _)
   | Psth(_, c, _) 
   | Pstw(_, c, _) 
+  | Pstw_a(_, c, _) 
   | Psubfic(_, _, c)
   | Pxori(_, _, c)
   | Pxoris(_, _, c) -> referenced_constant c