diff options
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | riscV/Asmgenproof1.v | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 50dc20be..329dd34c 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -170,8 +170,8 @@ let memcpy_small_arg sz arg tmp = assert false let expand_builtin_memcpy_small sz al src dst = - let (tsrc, tdst) = - if dst <> BA (IR X5) then (X5, X6) else (X6, X5) in + let tsrc = if dst <> BA (IR X5) then X5 else X6 in + let tdst = if src <> BA (IR X6) then X6 else X5 in let (rsrc, osrc) = memcpy_small_arg sz src tsrc in let (rdst, odst) = memcpy_small_arg sz dst tdst in let rec copy osrc odst sz = diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 42ab8375..89a48aee 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1147,14 +1147,14 @@ Opaque Int.eq. split; intros; Simpl. assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. compute; intuition congruence. } (* cast16signed *) { econstructor; split. eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. split; intros; Simpl. assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. compute; intuition congruence. } (* addimm *) { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). |