Changeset 1255 for src/joint

Timestamp:

Sep 22, 2011, 4:23:05 PM (9 years ago)

Author:

sacerdot

Message:

Major mistake fixed: op1 and op2 were assuming the source and dest registers
to be always the same. This is true only from LTL on.

File:

• src/joint/Joint.ma (modified) (1 diff)

src/joint/Joint.ma

@@ -35 +35 @@
   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
   | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
-  | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
-  | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
+  | joint_instr_op1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
+  | joint_instr_op2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
   | joint_instr_clear_carry: joint_instruction p globals
   | joint_instr_set_carry: joint_instruction p globals