From 1fc9e3b1f4cf32e88888c5277894f5ed1e74f7af Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 23 Nov 2020 22:21:23 +0100 Subject: bug #223 fix on PPC --- powerpc/CSE2deps.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'powerpc/CSE2deps.v') diff --git a/powerpc/CSE2deps.v b/powerpc/CSE2deps.v index d48dabf3..4592f408 100644 --- a/powerpc/CSE2deps.v +++ b/powerpc/CSE2deps.v @@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := (base :: nil), (base' :: nil) => if peq base base' then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk) - else true | _, _, _, _ => true + else true + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true end. -- cgit