aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selection.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Selection.v')
-rw-r--r--backend/Selection.v6
1 files changed, 5 insertions, 1 deletions
diff --git a/backend/Selection.v b/backend/Selection.v
index ca1f1619..e4be867f 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -348,7 +348,11 @@ Inductive stmt_class : Type :=
Fixpoint classify_stmt (s: Cminor.stmt) : stmt_class :=
match s with
| Cminor.Sskip => SCskip
- | Cminor.Sassign id a => SCassign id a
+ | Cminor.Sassign id a =>
+ match a with
+ | Cminor.Evar id2 => if ident_eq id id2 then SCskip else SCassign id a
+ | _ => SCassign id a
+ end
| Cminor.Sbuiltin None (EF_debug _ _ _) _ => SCskip
| Cminor.Sseq s1 s2 =>
match classify_stmt s1, classify_stmt s2 with