diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:26:46 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:26:46 +0200 |
| commit | 3bef0962079cf971673b4267b0142bd5fe092509 (patch) | |
| tree | 6dd283fa6b8305d960fd08938fbbd09e0940c139 /powerpc/NeedOp.v | |
| parent | e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (diff) | |
| download | compcert-kvx-3bef0962079cf971673b4267b0142bd5fe092509.tar.gz compcert-kvx-3bef0962079cf971673b4267b0142bd5fe092509.zip | |
Support for 64-bit architectures: update the PowerPC port
The PowerPC port remains 32-bit only, no support is added for PPC 64.
This shows how much work is needed to update an existing port a minima.
Diffstat (limited to 'powerpc/NeedOp.v')
| -rw-r--r-- | powerpc/NeedOp.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 4d8c32bd..956b5d43 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -108,11 +108,11 @@ Qed. Lemma needs_of_operation_sound: forall op args v nv args', - eval_operation ge (Vptr sp Int.zero) op args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> vagree_list args args' (needs_of_operation op nv) -> nv <> Nothing -> exists v', - eval_operation ge (Vptr sp Int.zero) op args' m' = Some v' + eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v' /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); @@ -147,7 +147,7 @@ Qed. Lemma operation_is_redundant_sound: forall op nv arg1 args v arg1' args', operation_is_redundant op nv = true -> - eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v -> vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. |