diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-05-03 11:18:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-03 11:18:32 +0200 |
| commit | 7873af34a9520ee5a8a6f10faddf3255a4ff02b2 (patch) | |
| tree | 74500c845c99b39ba91a5507656060dea60404ea /backend/Inliningspec.v | |
| parent | 25ea686abc4cce13aba92196dbeb284f727b6e0e (diff) | |
| download | compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.tar.gz compcert-kvx-7873af34a9520ee5a8a6f10faddf3255a4ff02b2.zip | |
Hybrid 64bit/32bit PowerPC port
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
Diffstat (limited to 'backend/Inliningspec.v')
| -rw-r--r-- | backend/Inliningspec.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 331f8b06..dfd96333 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -52,9 +52,9 @@ Proof. P dm fenv -> P (fold_left (fun x idg => PTree.set (fst idg) (snd idg) x) l dm) (fold_left add_globdef l fenv)). - { induction l; simpl; intros. + { induction l; simpl; intros. - auto. - - apply IHl. apply ADD; auto. + - apply IHl. apply ADD; auto. } intros. apply REC. red; intros. rewrite PTree.gempty in H; discriminate. Qed. @@ -63,8 +63,8 @@ Lemma fenv_compat_linkorder: forall cunit prog fenv, linkorder cunit prog -> fenv_compat cunit fenv -> fenv_compat prog fenv. Proof. - intros; red; intros. apply H0 in H1. - destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). + intros; red; intros. apply H0 in H1. + destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). inv Q. inv H3. auto. Qed. @@ -702,7 +702,7 @@ Lemma tr_function_linkorder: tr_function cunit f f' -> tr_function prog f f'. Proof. - intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. + intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. Qed. Lemma transf_function_spec: |