diff options
Diffstat (limited to 'cfrontend/SimplExprspec.v')
| -rw-r--r-- | cfrontend/SimplExprspec.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 453a4c9a..e317a728 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -411,6 +411,9 @@ Inductive tr_stmt: Csyntax.statement -> statement -> Prop := | tr_seq: forall s1 s2 ts1 ts2, tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> tr_stmt (Csyntax.Ssequence s1 s2) (Ssequence ts1 ts2) + | tr_ifthenelse_empty: forall r s' a, + tr_expression r s' a -> + tr_stmt (Csyntax.Sifthenelse r Csyntax.Sskip Csyntax.Sskip) (Ssequence s' Sskip) | tr_ifthenelse: forall r s1 s2 s' a ts1 ts2, tr_expression r s' a -> tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> @@ -1058,11 +1061,12 @@ Opaque transl_expression transl_expr_stmt. clear transl_stmt_meets_spec. induction s; simpl; intros until I; intros TR; try (monadInv TR); try (constructor; eauto). + destruct (is_Sskip s1); destruct (is_Sskip s2) eqn:?; monadInv EQ3; try (constructor; eauto). + eapply tr_ifthenelse_empty; eauto. destruct (is_Sskip s1); monadInv EQ4. apply tr_for_1; eauto. apply tr_for_2; eauto. destruct o; monadInv TR; constructor; eauto. - clear transl_lblstmt_meets_spec. induction s; simpl; intros until I; intros TR; monadInv TR; constructor; eauto. @@ -1108,4 +1112,3 @@ Proof. Qed. End SPEC. - |