@@ -458,18 +458,21 @@ object (self:'a)
458458 TR. tprop
459459 (floc#env#mk_global_variable dw#to_numerical)
460460 (__FILE__ ^ " :" ^ (string_of_int __LINE__))
461- | ARMOffsetAddress (r , align , offset , isadd , _iswback , _isindex , size ) ->
461+ | ARMOffsetAddress (r , align , offset , isadd , _iswback , isindex , size ) ->
462462 (match offset with
463463 | ARMImmOffset _ ->
464464 let rvar = env#mk_arm_register_variable r in
465465 let numoffset_r =
466- match (offset, isadd) with
467- | (ARMImmOffset i , true ) -> Ok (mkNumerical i)
468- | (ARMImmOffset i , false ) -> Ok (mkNumerical i)#neg
469- | _ ->
470- Error [__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : "
471- ^ " Immediate offset not yet implemented for offset "
472- ^ (arm_memory_offset_to_string offset)] in
466+ if isindex then
467+ match (offset, isadd) with
468+ | (ARMImmOffset i , true ) -> Ok (mkNumerical i)
469+ | (ARMImmOffset i , false ) -> Ok (mkNumerical i)#neg
470+ | _ ->
471+ Error [__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : "
472+ ^ " Immediate offset not yet implemented for offset "
473+ ^ (arm_memory_offset_to_string offset)]
474+ else
475+ Ok numerical_zero in
473476 TR. tbind
474477 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
475478 (fun memoff ->
@@ -1131,22 +1134,22 @@ let arm_sp_deref ?(with_offset=0) (mode:arm_operand_mode_t) =
11311134 if with_offset > = 0 then
11321135 let offset = ARMImmOffset with_offset in
11331136 mk_arm_offset_address_op
1134- ARSP offset ~isadd: true ~iswback: false ~isindex: false mode
1137+ ARSP offset ~isadd: true ~iswback: false ~isindex: true mode
11351138 else
11361139 let offset = ARMImmOffset (- with_offset) in
11371140 mk_arm_offset_address_op
1138- ARSP offset ~isadd: false ~iswback: false ~isindex: false mode
1141+ ARSP offset ~isadd: false ~iswback: false ~isindex: true mode
11391142
11401143
11411144let arm_reg_deref ?(with_offset =0 ) (reg : arm_reg_t ) (mode :arm_operand_mode_t ) =
11421145 if with_offset > = 0 then
11431146 let offset = ARMImmOffset with_offset in
11441147 mk_arm_offset_address_op
1145- reg offset ~isadd: true ~iswback: false ~isindex: false mode
1148+ reg offset ~isadd: true ~iswback: false ~isindex: true mode
11461149 else
11471150 let offset = ARMImmOffset (- with_offset) in
11481151 mk_arm_offset_address_op
1149- reg offset ~isadd: false ~iswback: false ~isindex: false mode
1152+ reg offset ~isadd: false ~iswback: false ~isindex: true mode
11501153
11511154
11521155let equal_register_lists (op1 : arm_operand_int ) (op2 : arm_operand_int ): bool =
0 commit comments