diff options
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 74101f53..e91c6ae1 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -89,6 +89,7 @@ Inductive operation : Type := | Oshru (**r [rd = r1 >> r2] (unsigned) *) | Oshruimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Oshrximm (n: int) (**r [rd = r1 / 2^n] (signed) *) + | Ororimm (n: int) (**r rotate right immediate *) (*c 64-bit integer arithmetic: *) | Omakelong (**r [rd = r1 << 32 | r2] *) | Olowlong (**r [rd = low-word(r1)] *) @@ -414,6 +415,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshru => (Tint :: Tint :: nil, Tint) | Oshruimm _ => (Tint :: nil, Tint) | Oshrximm _ => (Tint :: nil, Tint) + | Ororimm _ => (Tint :: nil, Tint) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) | Ohighlong => (Tlong :: nil, Tint) |