File tree Expand file tree Collapse file tree 1 file changed +13
-0
lines changed
Expand file tree Collapse file tree 1 file changed +13
-0
lines changed Original file line number Diff line number Diff line change @@ -1128,6 +1128,19 @@ object (self)
11281128 ~error: (fun e -> log_error_result __FILE__ __LINE__ e)
11291129 xtype_r);
11301130
1131+ (* LDRH rt, ... : X_rt <: integer type *)
1132+ (let tc = mk_int_type_constant SignedNeutral 16 in
1133+ let tctypeterm = mk_cty_term tc in
1134+ let rttypeterm = mk_vty_term rttypevar in
1135+ let rule = " LDRH-def-lhs" in
1136+ if fndata#is_typing_rule_enabled iaddr rule then
1137+ begin
1138+ log_subtype_constraint __LINE__ rule tctypeterm rttypeterm;
1139+ store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm
1140+ end
1141+ else
1142+ log_subtype_rule_disabled __LINE__ rule tctypeterm rttypeterm);
1143+
11311144 (* LDRH rt, [rn, rm] : X_rndef.load <: X_rt *)
11321145 (let xrdef = get_variable_rdefs_r (rn#to_variable floc) in
11331146 let rnreg = rn#to_register in
You can’t perform that action at this time.
0 commit comments