diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 09:49:45 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 09:49:45 +0100 |
| commit | a0c25ff1259a8373fb71e780f70d28916c321612 (patch) | |
| tree | 043fdf2bf1c56844d37603b13f7684858edf2155 /mppa_k1c/SelectLong.vp | |
| parent | 5487cf64164eeea716e3ad140977aa73ccbe00ce (diff) | |
| download | compcert-kvx-a0c25ff1259a8373fb71e780f70d28916c321612.tar.gz compcert-kvx-a0c25ff1259a8373fb71e780f70d28916c321612.zip | |
maddl / maddlim are synthesized (but not for pointers it seems)
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 07ebf1a2..3a17ab17 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -88,6 +88,14 @@ Nondetfunction addl (e1: expr) (e2: expr) := addlimm n1 (Eop Oaddl (t1:::t2:::Enil)) | t1, Eop (Oaddlimm n2) (t2:::Enil) => addlimm n2 (Eop Oaddl (t1:::t2:::Enil)) + | t1, (Eop Omull (t2:::t3:::Enil)) => + Eop Omaddl (t1:::t2:::t3:::Enil) + | (Eop Omull (t2:::t3:::Enil)), t1 => + Eop Omaddl (t1:::t2:::t3:::Enil) + | t1, (Eop (Omullimm n) (t2:::Enil)) => + Eop (Omaddlimm n) (t1:::t2:::Enil) + | (Eop (Omullimm n) (t2:::Enil)), t1 => + Eop (Omaddlimm n) (t1:::t2:::Enil) | _, _ => Eop Oaddl (e1:::e2:::Enil) end. |