From 76d82e41797ef79531e6bf3d530f380dddd3310e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 7 Sep 2015 15:51:45 +0200 Subject: Added builtin for the cmpb instruction. --- powerpc/Asm.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'powerpc/Asm.v') 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 _ _ _ -- cgit