diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-15 12:32:09 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-15 12:32:09 +0200 |
| commit | fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49 (patch) | |
| tree | ad4b3da06dc7621ed64353b52abb92edc8291ff6 /powerpc/Asm.v | |
| parent | 9dc0dd73f75875b301c886df40087192d0fad386 (diff) | |
| download | compcert-fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49.tar.gz compcert-fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49.zip | |
Removed usage of bne and removed duplicated code for return values of atomics.
Instead of introducing a new bne instruction in Asm.v and the TargetPrinter.ml
I use the equivalent bf instruction. The duplicated code is due to unused return
values of builtins. Now we only emit the additional code for the return value if
the return value is used instead of duplicating the whole emiting sequence.
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 _ _ _ |