diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-10-27 16:26:08 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-10-27 16:26:08 +0200 |
| commit | 9922feea537ced718a3822dd50eabc87da060338 (patch) | |
| tree | 6f67bb6707ef59e50d6bb81c61b2ed0b3c6097ab /arm/NeedOp.v | |
| parent | f2d6637c7d4a11f961ff289e64f70bf4de93d0aa (diff) | |
| parent | d50773e537ec6729f9152b545c6f938ab19eb7b8 (diff) | |
| download | compcert-9922feea537ced718a3822dd50eabc87da060338.tar.gz compcert-9922feea537ced718a3822dd50eabc87da060338.zip | |
Merge pull request #145 from AbsInt/64
Support for 64-bit target processors + support for x86 in 64-bit mode
Diffstat (limited to 'arm/NeedOp.v')
| -rw-r--r-- | arm/NeedOp.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/arm/NeedOp.v b/arm/NeedOp.v index 41b80941..dee7cae1 100644 --- a/arm/NeedOp.v +++ b/arm/NeedOp.v @@ -145,11 +145,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); @@ -188,7 +188,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. |