diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-24 23:53:42 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-24 23:53:42 +0100 |
| commit | 6a05fbf4b55dfdf2884c3e0b2cb57d707ad1598d (patch) | |
| tree | 4b2c636ff0dcb101819bfbacbd5f07d2bff5d72f /aarch64/Asmgenproof1.v | |
| parent | 2729bdeb4aced04a1301d5696574ff8610072395 (diff) | |
| download | compcert-kvx-6a05fbf4b55dfdf2884c3e0b2cb57d707ad1598d.tar.gz compcert-kvx-6a05fbf4b55dfdf2884c3e0b2cb57d707ad1598d.zip | |
Asmgenproof1
Diffstat (limited to 'aarch64/Asmgenproof1.v')
| -rw-r--r-- | aarch64/Asmgenproof1.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 4da1b52b..bd1474b6 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -1932,7 +1932,9 @@ Proof. { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. } destruct offset_representable. - econstructor; econstructor; split. apply exec_straight_opt_refl. auto. -- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C). +- exploit (exec_loadimm64 X16); eauto. + simpl. congruence. + intros (rs' & A & B & C). econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. split. simpl. rewrite B, C by eauto with asmgen. auto. auto. Qed. |