diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-12 17:11:24 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-12 17:11:24 +0100 |
commit | 1c477f375f20e882b429175c737ad013ff202c0b (patch) | |
tree | b22df7e783c21edc70f9354e7eedb2ecf29a56de /riscV/ConstpropOpproof.v | |
parent | e6308c5ec63a3a01ee33c9304e5249c6159dd1ef (diff) | |
download | compcert-1c477f375f20e882b429175c737ad013ff202c0b.tar.gz compcert-1c477f375f20e882b429175c737ad013ff202c0b.zip |
Introduce more brackets for register annotation.
It seems necessary that the mulitplication for the high part of
split registers is put into brackets.
Bug 23169
Diffstat (limited to 'riscV/ConstpropOpproof.v')
0 files changed, 0 insertions, 0 deletions