diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 11:57:09 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-11 11:57:09 +0200 |
| commit | e93ef3ef5f0925ce6b99208157a49a99032c1f87 (patch) | |
| tree | e23eaf50b40e6bfdeee8e9fe3da9a840269f5401 /mppa_k1c/Asm.v | |
| parent | cdb5ec57d700c5409c0717bb99258a5effed9601 (diff) | |
| download | compcert-kvx-e93ef3ef5f0925ce6b99208157a49a99032c1f87.tar.gz compcert-kvx-e93ef3ef5f0925ce6b99208157a49a99032c1f87.zip | |
__builtin_k1_ldu
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 9517099c..26c6cc02 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -72,13 +72,15 @@ Inductive instruction : Type := | 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 *)
| Pjumptable (r: ireg) (labels: list label)
-
+
+ (* For builtins *)
| Ploopdo (count: ireg) (loopend: label)
| Pgetn (n: int) (dst: ireg)
| Psetn (n: int) (src: ireg)
| Pwfxl (n: int) (src: ireg)
| Pwfxm (n: int) (src: ireg)
-
+ | Pldu (dst: ireg) (addr: ireg)
+
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
| Plbu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *)
|