diff options
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 5fd40a27..3c7bdd15 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -153,8 +153,6 @@ Inductive instruction : Type := | Pbdnz: label -> instruction (**r decrement CTR and branch if not zero *) | Pbf: crbit -> label -> instruction (**r branch if false *) | Pbl: ident -> signature -> instruction (**r branch and link *) - | Pbne: label -> instruction (**r branch not equal *) - | Pbne_rel: int -> instruction (**r branch not equal with relative offset *) | Pbs: ident -> signature -> instruction (**r branch to symbol *) | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) @@ -875,8 +873,6 @@ 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 _ - | Pbne _ - | Pbne_rel _ | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ |