Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


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

1 files changed, 4 insertions, 2 deletions

diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index b8611075..b95ad669 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -91,11 +91,13 @@ Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) :=
   | _, _ => Unknown
   end.
 
+Parameter propagate_float_constants: unit -> bool.
+
 Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   match op, vl with
   | Omove, v1::nil => v1
   | Ointconst n, nil => I n
-  | Ofloatconst n, nil => F n
+  | Ofloatconst n, nil => if propagate_float_constants tt then F n else Unknown
   | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1)
   | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n1)
   | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n1)
@@ -132,7 +134,7 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
   | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
-  | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
+  | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown
   | Ocmp c, vl => eval_static_condition_val c vl
   | _, _ => Unknown
   end.