diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-20 13:05:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-20 13:05:53 +0000 |
| commit | 7698300cfe2d3f944ce2e1d4a60a263620487718 (patch) | |
| tree | 74292bb5f65bc797906b5c768df2e2e937e869b6 /ia32/SelectOp.vp | |
| parent | c511207bd0f25c4199770233175924a725526bd3 (diff) | |
| download | compcert-7698300cfe2d3f944ce2e1d4a60a263620487718.tar.gz compcert-7698300cfe2d3f944ce2e1d4a60a263620487718.zip | |
Merge of branch value-analysis.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/SelectOp.vp')
| -rw-r--r-- | ia32/SelectOp.vp | 18 |
1 files changed, 3 insertions, 15 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 1471405e..d8a21271 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -71,24 +71,12 @@ Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil). (** ** Integer addition and pointer addition *) -Definition offset_addressing (a: addressing) (ofs: int) : addressing := - match a with - | Aindexed n => Aindexed (Int.add n ofs) - | Aindexed2 n => Aindexed2 (Int.add n ofs) - | Ascaled sc n => Ascaled sc (Int.add n ofs) - | Aindexed2scaled sc n => Aindexed2scaled sc (Int.add n ofs) - | Aglobal id n => Aglobal id (Int.add n ofs) - | Abased id n => Abased id (Int.add n ofs) - | Abasedscaled sc id n => Abasedscaled sc id (Int.add n ofs) - | Ainstack n => Ainstack (Int.add n ofs) - end. - Nondetfunction addimm (n: int) (e: expr) := if Int.eq n Int.zero then e else match e with - | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Olea addr) args => Eop (Olea (offset_addressing addr n)) args - | _ => Eop (Olea (Aindexed n)) (e ::: Enil) + | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil + | Eop (Olea addr) args => Eop (Olea (offset_addressing_total addr n)) args + | _ => Eop (Olea (Aindexed n)) (e ::: Enil) end. Nondetfunction add (e1: expr) (e2: expr) := |