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/Conventions.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/Conventions.v')
| -rw-r--r-- | backend/Conventions.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Conventions.v b/backend/Conventions.v index 64a83a58..bdc4c8b6 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -33,7 +33,7 @@ Proof. exploit H; eauto. destruct p; simpl in *; intuition congruence. apply IHpl; auto. Qed. - + (** ** Location of function parameters *) (** A function finds the values of its parameter in the same locations @@ -65,7 +65,7 @@ Proof. inv A. auto. unfold loc_parameters. generalize (loc_arguments sg). induction l as [ | p l]; simpl; intros. auto. - rewrite map_app. f_equal; auto. destruct p; auto. + rewrite map_app. f_equal; auto. destruct p; auto. Qed. (** * Tail calls *) @@ -90,8 +90,8 @@ Definition tailcall_is_possible (sg: signature) : bool := Lemma tailcall_is_possible_correct: forall s, tailcall_is_possible s = true -> tailcall_possible s. Proof. - unfold tailcall_is_possible; intros. rewrite forallb_forall in H. - red; intros. apply H in H0. destruct l; [auto|discriminate]. + unfold tailcall_is_possible; intros. rewrite forallb_forall in H. + red; intros. apply H in H0. destruct l; [auto|discriminate]. Qed. Lemma zero_size_arguments_tailcall_possible: |