diff options
Diffstat (limited to 'backend/RTLtypingaux.ml')
| -rw-r--r-- | backend/RTLtypingaux.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 657c4da..7549ff4 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -45,6 +45,8 @@ let type_instr retty (Coq_pair(pc, i)) = | Iop(Omove, _, _, _) -> () | Iop(op, args, res, _) -> + if two_address_op op && List.length args >= 1 && List.hd args <> res + then raise (Type_error "two-address constraint violation"); let (Coq_pair(targs, tres)) = type_of_operation op in set_types args targs; set_type res tres | Iload(chunk, addr, args, dst, _) -> |