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 /backend/AisAnnot.ml | |
| parent | e6308c5ec63a3a01ee33c9304e5249c6159dd1ef (diff) | |
| download | compcert-kvx-1c477f375f20e882b429175c737ad013ff202c0b.tar.gz compcert-kvx-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 'backend/AisAnnot.ml')
| -rw-r--r-- | backend/AisAnnot.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml index 4c637922..fc3c0305 100644 --- a/backend/AisAnnot.ml +++ b/backend/AisAnnot.ml @@ -77,15 +77,16 @@ let ais_expr_arg pos preg_string sp_reg_name arg = | BA_addrglobal(id, ofs) -> addr_global id ofs | BA_splitlong(hi, lo) -> - combine " * 0x100000000 + " hi lo + let arg1 = combine " * " (ais_arg hi) (simple "0x100000000") in + combine " + " arg1 (ais_arg lo) | BA_addptr(a1, a2) -> + let a1 = ais_arg a1 + and a2 = ais_arg a2 in combine " + " a1 a2 and combine mid arg1 arg2 = let op_br = simple "(" and mid = simple mid - and cl_br = simple ")" - and arg1 = ais_arg arg1 - and arg2 = ais_arg arg2 in + and cl_br = simple ")" in op_br@arg1@mid@arg2@cl_br in ais_arg arg |