diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2021-08-11 15:21:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-06 14:33:45 +0200 |
| commit | 7e8e3efdd69cee4412817f2e29f9ef687bec019b (patch) | |
| tree | e758a33cc8066b230aea40625a28e71458b4f566 /powerpc/Asmgenproof.v | |
| parent | a320361a90efaa48275153f2e19ccfb443b32688 (diff) | |
| download | compcert-kvx-7e8e3efdd69cee4412817f2e29f9ef687bec019b.tar.gz compcert-kvx-7e8e3efdd69cee4412817f2e29f9ef687bec019b.zip | |
Share code for memory access for PowerPC
Instead of duplicating the memory access code in `Asmexpand.ml` we move
the code for each of the different addressings in `Asmgen.v` into
separate functions that then can be reused in `Asmexpand.ml`.
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 2730e3d6..85541118 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. |