From a3be6358778bb02b03b62486a60b9fd9ef1f1c04 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 12 Mar 2020 11:37:59 +0100 Subject: more lemmas --- backend/CSE3analysis.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'backend/CSE3analysis.v') 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. -- cgit