diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 11:37:59 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 11:37:59 +0100 |
| commit | a3be6358778bb02b03b62486a60b9fd9ef1f1c04 (patch) | |
| tree | a88730ada5a8c405c8e322a13486caeb07cbd8d9 /backend/CSE3analysis.v | |
| parent | ee3bc59771eb50a8e39dc1db21e5439ce992e630 (diff) | |
| download | compcert-kvx-a3be6358778bb02b03b62486a60b9fd9ef1f1c04.tar.gz compcert-kvx-a3be6358778bb02b03b62486a60b9fd9ef1f1c04.zip | |
more lemmas
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 2d559413..a85cd493 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -286,12 +286,15 @@ Section OPERATIONS. (src : reg) (ty: typ) (rel : RELATION.t) : RELATION.t := let rel' := store2 chunk addr args src rel in - match eq_find {| eq_lhs := src; - eq_op := SLoad chunk addr; - eq_args:= args |} with - | Some id => PSet.add id rel' - | None => rel' - end. + if loadv_storev_compatible_type chunk ty + then + match eq_find {| eq_lhs := src; + eq_op := SLoad chunk addr; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end + else rel'. End PER_NODE. |