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/SelectOpproof.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/SelectOpproof.v')
0 files changed, 0 insertions, 0 deletions