diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 09:39:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 09:39:03 +0100 |
| commit | af7afc0a388986a94f21d2657cc13b823d456781 (patch) | |
| tree | b05b51925b869913faa19e381daf5ab1f8b62e53 /backend/CSE2.v | |
| parent | c4f88ed5581ffb71e7ed5824c7503e8ce08165df (diff) | |
| download | compcert-kvx-af7afc0a388986a94f21d2657cc13b823d456781.tar.gz compcert-kvx-af7afc0a388986a94f21d2657cc13b823d456781.zip | |
offsets in globals for x86
Diffstat (limited to 'backend/CSE2.v')
| -rw-r--r-- | backend/CSE2.v | 5 |
1 files changed, 4 insertions, 1 deletions
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. |