diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-07 15:51:45 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-07 15:51:45 +0200 |
| commit | 76d82e41797ef79531e6bf3d530f380dddd3310e (patch) | |
| tree | e166104322f4bb427993cf483623e0a01632c1b4 /powerpc/Asm.v | |
| parent | 9ecede34667433bc3cacf47fb75e03a79607223b (diff) | |
| download | compcert-kvx-76d82e41797ef79531e6bf3d530f380dddd3310e.tar.gz compcert-kvx-76d82e41797ef79531e6bf3d530f380dddd3310e.zip | |
Added builtin for the cmpb instruction.
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 863ed6a1..2ad99304 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -157,6 +157,7 @@ Inductive instruction : Type := | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table (pseudo) *) + | Pcmpb: ireg -> ireg -> ireg -> instruction (**r compare bytes *) | Pcmplw: ireg -> ireg -> instruction (**r unsigned integer comparison *) | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) @@ -871,6 +872,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** The following instructions and directives are not generated directly by [Asmgen], so we do not model them. *) | Pbdnz _ + | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ |