diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-07-12 14:05:06 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-07-12 14:05:06 +0200 |
commit | 2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e (patch) | |
tree | 8f7f5d59c692ee8f548a0695d14eb89cccf951c5 /lib/Intv.v | |
parent | 0d783f1aa5e4f94b713588fb272ecca6a1bc23ca (diff) | |
download | compcert-2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e.tar.gz compcert-2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e.zip |
Constprop strength reduction (#17)
PowerPC port: add strength reduction for 64-bit operations
* Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748)
* Moved shru_rolml proof to Values.
Diffstat (limited to 'lib/Intv.v')
0 files changed, 0 insertions, 0 deletions