diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 22:29:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 22:29:14 +0200 |
| commit | 4571fc5fade196c02d68c4feb5e5a1b862d37041 (patch) | |
| tree | 681f4992fee674059d6f8245e9e2b6da35256e2f /mppa_k1c/Asm.v | |
| parent | 9cdb61cc69db8fbb9bedfd3957b9512f8622fb7a (diff) | |
| download | compcert-kvx-4571fc5fade196c02d68c4feb5e5a1b862d37041.tar.gz compcert-kvx-4571fc5fade196c02d68c4feb5e5a1b862d37041.zip | |
more builtins
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index a9a88d75..f679335c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -80,6 +80,9 @@ Inductive instruction : Type := | Pwfxl (n: int) (src: ireg)
| Pwfxm (n: int) (src: ireg)
| Pldu (dst: ireg) (addr: ireg)
+ | Plbzu (dst: ireg) (addr: ireg)
+ | Plhzu (dst: ireg) (addr: ireg)
+ | Plwzu (dst: ireg) (addr: ireg)
| Pawait
| Psleep
| Pstop
@@ -94,6 +97,8 @@ Inductive instruction : Type := | Pdzerol (addr: ireg)
| Pafaddd (addr: ireg) (incr_res: ireg)
| Pafaddw (addr: ireg) (incr_res: ireg)
+ | Palclrd (dst: ireg) (addr: ireg)
+ | Palclrw (dst: ireg) (addr: ireg)
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
|