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 /common/Smallstep.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 'common/Smallstep.v')
| -rw-r--r-- | common/Smallstep.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/common/Smallstep.v b/common/Smallstep.v index 9c91243a..c269013b 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -786,7 +786,7 @@ End SIMULATION_SEQUENCES. Lemma compose_forward_simulations: forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3. Proof. - intros L1 L2 L3 S12 S23. + intros L1 L2 L3 S12 S23. destruct S12 as [index order match_states props]. destruct S23 as [index' order' match_states' props']. @@ -1632,7 +1632,7 @@ Theorem factor_forward_simulation: forward_simulation L1 L2 -> single_events L2 -> forward_simulation (atomic L1) L2. Proof. - intros L1 L2 FS L2single. + intros L1 L2 FS L2single. destruct FS as [index order match_states sim]. apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor. - (* wf *) @@ -1727,7 +1727,7 @@ Theorem factor_backward_simulation: backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 -> backward_simulation L1 (atomic L2). Proof. - intros L1 L2 BS L1single L2wb. + intros L1 L2 BS L1single L2wb. destruct BS as [index order match_states sim]. apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor. - (* wf *) |