diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 12:14:33 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 12:14:33 +0200 |
| commit | 71bfa128316019b0199db87acdf31deb9f9e7405 (patch) | |
| tree | 141abac0b985cbf2904e68df40309fb9fda18cfc /mppa_k1c/Asm.v | |
| parent | e93ef3ef5f0925ce6b99208157a49a99032c1f87 (diff) | |
| download | compcert-kvx-71bfa128316019b0199db87acdf31deb9f9e7405.tar.gz compcert-kvx-71bfa128316019b0199db87acdf31deb9f9e7405.zip | |
some 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 26c6cc02..55138a3f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -80,6 +80,11 @@ Inductive instruction : Type := | Pwfxl (n: int) (src: ireg)
| Pwfxm (n: int) (src: ireg)
| Pldu (dst: ireg) (addr: ireg)
+ | Pawait
+ | Psleep
+ | Pstop
+ | Pbarrier
+ | Pfence
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
|