diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 0f6f2b8b..d2d562c8 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -65,6 +65,7 @@ Inductive instruction : Type := | Pj_l (l: label) (**r jump to label *)
| Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *)
| Pcbu (bt: btest) (r: ireg) (l: label) (**r branch based on btest with unsigned semantics *)
+ | Ploopdo (count: ireg) (loopend: label)
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte *)
@@ -147,7 +148,7 @@ Inductive instruction : Type := | Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *)
| Pandil (rd rs: ireg) (imm: int64) (**r and immediate long *)
| Poril (rd rs: ireg) (imm: int64) (**r or immediate long *)
- | Pxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
+ | Pxoril (rd rs: ireg) (imm: int64) (**r xor immediate long *)
.
(** Correspondance between Asmblock and Asm *)
|