diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
commit | 202bc495442a1a8fa184b73ac0063bdbbbcdf846 (patch) | |
tree | 46c6920201b823bf47252bc52864b0bf60f3233e /ia32/ConstpropOp.vp | |
parent | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (diff) |
Constant propagation within __builtin_annot.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/ConstpropOp.vp')
-rw-r--r-- | ia32/ConstpropOp.vp | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index 8a612f0..e6ba98a 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -307,15 +307,4 @@ Nondetfunction op_strength_reduction | _, _, _ => (op, args) end. -Nondetfunction builtin_strength_reduction - (ef: external_function) (args: list reg) (vl: list approx) := - match ef, args, vl with - | EF_vload chunk, r1 :: nil, G symb n1 :: nil => - (EF_vload_global chunk symb n1, nil) - | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => - (EF_vstore_global chunk symb n1, r2 :: nil) - | _, _, _ => - (ef, args) - end. - End STRENGTH_REDUCTION. |