From d4f3b8645c3c94cc376a8f35513bcb28da9b1722 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 23 Nov 2020 18:02:15 +0100 Subject: fix bug #223 on Risc-V --- riscV/CSE2deps.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'riscV/CSE2deps.v') diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v index b4b80e2f..c0deacf0 100644 --- a/riscV/CSE2deps.v +++ b/riscV/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 (Ptrofs.unsigned ofs') chunk' (Ptrofs.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