From 36c82ee8b0ac340a663a3790d70fd200d3f35ef9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 23 Nov 2020 17:32:00 +0100 Subject: correction bug #223 sur KVX --- kvx/CSE2deps.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kvx/CSE2deps.v') diff --git a/kvx/CSE2deps.v b/kvx/CSE2deps.v index b4b80e2f..c0deacf0 100644 --- a/kvx/CSE2deps.v +++ b/kvx/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