diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-26 23:46:47 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-26 23:46:47 +0100 |
| commit | 2e1912abc2d1f20f50d98c862c5ce9a961a3f3bf (patch) | |
| tree | fe3ac80585807dd91fab360c7b975f0d3420a218 /aarch64/Asmgenproof.v | |
| parent | df48280ac8a59754070dd1ad7db43f05fa0f9bcd (diff) | |
| parent | c7f3bd8555c1cae001cc93d21398b52b19d58df0 (diff) | |
| download | compcert-kvx-2e1912abc2d1f20f50d98c862c5ce9a961a3f3bf.tar.gz compcert-kvx-2e1912abc2d1f20f50d98c862c5ce9a961a3f3bf.zip | |
Merge branch 'aarch64_Pfmovimm_tuning' into aarch64-postpass
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index bbca6968..f0b09ef6 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -787,7 +787,7 @@ Proof. destruct ai; simpl; intros; try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate). - destruct i; simpl in BASIC; - unfold compare_long in BASIC; rewrite <- BASIC; + try destruct (negb _); rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. - destruct i; simpl in BASIC. 1,2: rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. @@ -1169,6 +1169,8 @@ Proof. try (destruct_reg_inv); try (inv_matchi); inversion BASIC; clear BASIC; subst; + try (destruct (is_immediate_float64 _)); + try (destruct (is_immediate_float32 _)); eexists; eexists; split; eauto; repeat (eapply match_internal_nextinstr_set_parallel; try congruence); try (econstructor; eauto); |