diff options
Diffstat (limited to 'riscV/SelectOp.vp')
| -rw-r--r-- | riscV/SelectOp.vp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index b38b7b4d..bb8af2ed 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -442,5 +442,9 @@ Nondetfunction builtin_arg (e: expr) := BA_long (Int64.ofwords h l) | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs + | Eop (Oaddimm n) (e1:::Enil) => + if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n) + | Eop (Oaddlimm n) (e1:::Enil) => + if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. |