diff options
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index a5bef9ae..8dfe29ef 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -345,12 +345,17 @@ Inductive stmt_class : Type := | SCassign (id: ident) (a: Cminor.expr) | SCother. -Function classify_stmt (s: Cminor.stmt) : stmt_class := +Fixpoint classify_stmt (s: Cminor.stmt) : stmt_class := match s with | Cminor.Sskip => SCskip | Cminor.Sassign id a => SCassign id a - | Cminor.Sseq Cminor.Sskip s => classify_stmt s - | Cminor.Sseq s Cminor.Sskip => classify_stmt s + | Cminor.Sbuiltin None (EF_debug _ _ _) _ => SCskip + | Cminor.Sseq s1 s2 => + match classify_stmt s1, classify_stmt s2 with + | SCskip, c2 => c2 + | c1, SCskip => c1 + | _, _ => SCother + end | _ => SCother end. |