diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-24 14:51:15 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-24 14:51:15 +0200 |
| commit | e49318b3606d7568d8592887e4278efa696afd10 (patch) | |
| tree | 99a9a1b883e1db3a4f56e1b5046453817827ceef /powerpc/Asmgenproof.v | |
| parent | 2789e6179af061381f5b18a268adb562b28bcb8e (diff) | |
| parent | c34d25e011402aedad62b3fe9b7b04989df4522e (diff) | |
| download | compcert-kvx-e49318b3606d7568d8592887e4278efa696afd10.tar.gz compcert-kvx-e49318b3606d7568d8592887e4278efa696afd10.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index e30ca9ed..e25ae583 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -310,7 +310,7 @@ Remark transl_memory_access_label: (forall r1 r2, nolabel (mk2 r1 r2)) -> tail_nolabel k c. Proof. - unfold transl_memory_access; intros; destruct addr; TailNoLabel. + unfold transl_memory_access, aindexed, aindexed2, aglobal, abased, ainstack; intros; destruct addr; TailNoLabel. destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero). destruct (Int.eq (high_s i) Int.zero); TailNoLabel. eapply tail_nolabel_trans. apply loadimm_label. TailNoLabel. destruct (symbol_is_small_data i i0). destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. |