diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:58:01 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:58:01 +0100 |
| commit | c4f88ed5581ffb71e7ed5824c7503e8ce08165df (patch) | |
| tree | 74794f389a24da51281d12456d3018c62929693f /backend/CSE2.v | |
| parent | a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08 (diff) | |
| download | compcert-kvx-c4f88ed5581ffb71e7ed5824c7503e8ce08165df.tar.gz compcert-kvx-c4f88ed5581ffb71e7ed5824c7503e8ce08165df.zip | |
globals alias analysis for x86
Diffstat (limited to 'backend/CSE2.v')
| -rw-r--r-- | backend/CSE2.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index f5ff8748..5b0556aa 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -288,6 +288,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := if peq base base' then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk) else true + | (Aglobal symb ofs), (Aglobal symb' ofs'), + nil, nil => peq symb symb' | _, _, _, _ => true end. |