diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-24 18:34:18 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-24 18:34:18 +0200 |
| commit | 7c62581ebd562a8baeebcb95c7624f53d46dd3ac (patch) | |
| tree | 707f7da4936e2f07bcd38be9cc7201cf63710da6 /kvx/Asmblockgenproof1.v | |
| parent | 159777cd07801bcc15d54363adf62cf91dd3fcba (diff) | |
| download | compcert-kvx-7c62581ebd562a8baeebcb95c7624f53d46dd3ac.tar.gz compcert-kvx-7c62581ebd562a8baeebcb95c7624f53d46dd3ac.zip | |
same changes as for RISC-V
Diffstat (limited to 'kvx/Asmblockgenproof1.v')
| -rw-r--r-- | kvx/Asmblockgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v index 259c4f9c..a18afec8 100644 --- a/kvx/Asmblockgenproof1.v +++ b/kvx/Asmblockgenproof1.v @@ -1521,14 +1521,14 @@ Opaque Int.eq. repeat split; intros; simpl; Simpl. assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. 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. - (* Ocast16signed *) econstructor; split. eapply exec_straight_two. simpl;eauto. simpl;eauto. repeat split; intros; Simpl. assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. 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. - (* Oshrximm *) econstructor; split. + apply exec_straight_one. simpl. eauto. |