diff options
Diffstat (limited to 'cfrontend/Cshmgenproof2.v')
| -rw-r--r-- | cfrontend/Cshmgenproof2.v | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index aa4e391a..6b7b5e3c 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -285,15 +285,24 @@ Lemma make_cmp_correct: eval_expr tprog e m c v. Proof. intros until m. intro SEM. unfold make_cmp. - functional inversion SEM; rewrite H0; intros. - inversion H8. eauto with cshm. + functional inversion SEM; rewrite H0; intros. + (* I32unsi *) inversion H8. eauto with cshm. + (* ipip int int *) inversion H8. eauto with cshm. - inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. functional inversion H; subst; unfold eval_compare_null; - rewrite H8; auto. + (* ipip ptr ptr *) inversion H10. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H3. unfold eq_block; rewrite H9. auto. + simpl. rewrite H3. unfold eq_block. rewrite H9. auto. + (* ipip ptr int *) + inversion H9. eapply eval_Ebinop; eauto with cshm. + simpl. unfold eval_compare_null. rewrite H8. + functional inversion H; subst; auto. + (* ipip int ptr *) + inversion H9. eapply eval_Ebinop; eauto with cshm. + simpl. unfold eval_compare_null. rewrite H8. + functional inversion H; subst; auto. + (* ff *) + inversion H8. eauto with cshm. Qed. Lemma transl_unop_correct: |