From af7afc0a388986a94f21d2657cc13b823d456781 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 3 Mar 2020 09:39:03 +0100 Subject: offsets in globals for x86 --- backend/CSE2.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 5b0556aa..9c45b476 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -289,7 +289,10 @@ Definition may_overlap chunk addr args chunk' addr' args' := then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk) else true | (Aglobal symb ofs), (Aglobal symb' ofs'), - nil, nil => peq symb symb' + nil, nil => + if peq symb symb' + then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + else false | _, _, _, _ => true end. -- cgit