Changeset 2176 for src/Clight/SimplifyCasts.ma
 Timestamp:
 Jul 12, 2012, 1:28:28 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r2103 r2176 719 719 #castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result 720 720 elim castee_val 721 [ 1:  2: #sz' #i  3: #f  4: #r 5: #ptr ]721 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ] 722 722 [ 2:  *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ] 723 723 whd in ⊢ ((??%?) → ?); … … 750 750 #sz #sg #v1 #v2 #m #r 751 751 elim v1 752 [ 1:  2: #sz' #i  3: #f  4: #r 5: #ptr ]752 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ] 753 753 whd in ⊢ ((??%?) → ?); normalize nodelta 754 754 >classify_add_int normalize nodelta #H destruct 755 755 elim v2 in H; 756 [ 1:  2: #sz'' #i'  3: #f'  4: #r' 5: #ptr' ]756 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ] 757 757 whd in ⊢ ((??%?) → ?); #H destruct 758 758 elim (sz_eq_dec sz' sz'') … … 766 766 #sz #sg #v1 #v2 #m #r 767 767 elim v1 768 [ 1:  2: #sz' #i  3: #f  4: #r 5: #ptr ]768 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ] 769 769 whd in ⊢ ((??%?) → ?); normalize nodelta 770 770 >classify_sub_int normalize nodelta #H destruct 771 771 elim v2 in H; 772 [ 1:  2: #sz'' #i'  3: #f'  4: #r' 5: #ptr' ]772 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ] 773 773 whd in ⊢ ((??%?) → ?); #H destruct 774 774 elim (sz_eq_dec sz' sz'') … … 789 789 #sz #sg #v1 #v2 #m 790 790 elim v1 791 [ 1:  2: #sz' #i  3: #f  4: #r 5: #ptr ]791 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ] 792 792 [ 2:  *: #_ %1 %1 % #H @H ] 793 793 elim v2 794 [ 1:  2: #sz'' #i'  3: #f'  4: #r' 5: #ptr' ]794 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ] 795 795 [ 2:  *: #_ %1 %2 % #H @H ] 796 796 whd in ⊢ ((??%?) → ?); normalize nodelta … … 808 808 #sz #sg #v1 #v2 #m 809 809 elim v1 810 [ 1:  2: #sz' #i  3: #f  4: #r 5: #ptr ]810 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ] 811 811 [ 2:  *: #_ %1 %1 % #H @H ] 812 812 elim v2 813 [ 1:  2: #sz'' #i'  3: #f'  4: #r' 5: #ptr' ]813 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ] 814 814 [ 2:  *: #_ %1 %2 % #H @H ] 815 815 whd in ⊢ ((??%?) → ?); normalize nodelta … … 827 827 elim op normalize in match (binop_simplifiable ?); #H destruct 828 828 elim v1 in H; 829 [ 1,6:  2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I))  3,8: #f  4,9: #r 5,10: #ptr ]829 [ 1,6:  2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I))  3,8: #f  4,9:  5,10: #ptr ] 830 830 #_ 831 831 whd in match (sem_binary_operation ??????); normalize nodelta … … 1186 1186  1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *) 1187 1187 #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep 1188 cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧ 1189 (pointer_compat_dec block r = inl ?? pc) ∧ 1190 (ty = Tpointer r ptype) ∧ 1191 val = Vptr (mk_pointer r block pc offset)) 1188 cut (∃block,offset,ptype. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧ 1189 (ty = Tpointer ptype) ∧ 1190 val = Vptr (mk_pointer block offset)) 1192 1191 [ 1: lapply Hstep Hstep 1193 1192 cases (exec_lvalue ge en m e1) 1194 1193 [ 1: * * #block #offset #trace' normalize nodelta 1195 1194 cases ty 1196 [ 2: #sz #sg  3: #fsz  4: # rg #ptr_ty  5: #rg#array_ty #array_sz  6: #domain #codomain1197  7: #structname #fieldspec  8: #unionname #fieldspec  9: # rg #id ]1195 [ 2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 1196  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] 1198 1197 normalize nodelta try (#Heq destruct) 1199 @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty) 1200 cases (pointer_compat_dec block rg) in Heq; normalize 1201 [ 2: #Hnotcompat #Hcontr destruct 1202  1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ] 1198 @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty) 1199 try @conj try @conj destruct // 1203 1200  2: normalize nodelta #errmesg #Hcontr destruct 1204 1201 ] 1205  2: * #block * #offset * # region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat#Hty_eq #Hval_eq1202  2: * #block * #offset * #ptype * * #Hexec_lvalue #Hty_eq #Hval_eq 1206 1203 whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta 1207 >Hptr_compat//1204 // 1208 1205 ] 1209 1206 ] … … 1644 1641 >Htype_eq 1645 1642 cases (typeof rec_expr1) normalize nodelta 1646 [ 2: #sz #sg  3: #fl  4: # rg #ty  5: #rg #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #rg#ty ]1643 [ 2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 1647 1644 [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/ 1648 1645  6,7: cases Hsim_lvalue … … 1659 1656 >Htype_eq 1660 1657 cases (typeof rec_expr1) normalize nodelta 1661 [ 2: #sz #sg  3: #fl  4: # rg #ty  5: #rg #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #rg#ty ]1658 [ 2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 1662 1659 [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/ 1663 1660  6,7: cases Hsim_lvalue … … 1931 1928 whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); 1932 1929 [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta 1933 [ 2: #sz #sg  3: #fl  4: # rg #ty'  5: #rg#ty #n  6: #tl #ty'1934  7: #id #fl  8: #id #fl  9: # rg #id ]1930 [ 2: #sz #sg  3: #fl  4: #ty'  5: #ty #n  6: #tl #ty' 1931  7: #id #fl  8: #id #fl  9: #id ] 1935 1932 try (@SimFail /2 by ex_intro/) 1936 1933 cases Hsim_lvalue … … 1943 1940  2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *) 1944 1941 >Htype_eq cases (typeof rec_expr1) normalize nodelta 1945 [ 2: #sz #sg  3: #fl  4: # rg #ty'  5: #rg#ty #n  6: #tl #ty'1946  7: #id #fl  8: #id #fl  9: # rg #id ]1942 [ 2: #sz #sg  3: #fl  4: #ty'  5: #ty #n  6: #tl #ty' 1943  7: #id #fl  8: #id #fl  9: #id ] 1947 1944 try (@SimFail /2 by ex_intro/) 1948 1945 cases Hsim_lvalue … … 2204 2201 normalize in match (typeof (Expr ??)); 2205 2202 cases ty' in Hsim_lvalue; normalize nodelta 2206 [ 2: #sz #sg  3: #fsz  4: # rg #ptr_ty  5: #rg#array_ty #array_sz  6: #domain #codomain2207  7: #structname #fieldspec  8: #unionname #fieldspec  9: # rg #id ]2203 [ 2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain 2204  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ] 2208 2205 #Hsim_lvalue 2209 2206 try (@SimFail /2 by ex_intro/) … … 2609 2606  3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd) 2610 2607  4: #r #Habsurd destruct (Habsurd) ] 2611  3: #irrelevant #Habsurd destruct 2612  5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct 2608  3,4,9: #irrelevant #Habsurd destruct 2613 2609  *: #irrelevant1 #irrelevant2 #Habsurd destruct ] 2614 2610  2: (* Kseq stm' k' *) … … 2675 2671 (free_list m (blocks_of_env en)))} @conj 2676 2672 [ 1: //  2: %3 @cc_call // ] 2677  3: #irrelevant #Habsurd destruct (Habsurd) 2678  5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct (Habsurd) 2673  3,4,9: #irrelevant #Habsurd destruct (Habsurd) 2679 2674  *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ] 2680 2675 ] … … 2904 2899 [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta 2905 2900 whd in match (ret ??) in ⊢ (% → %); 2906 [ 2: #sz #sg  3: #fl  4: # rg #ty'  5: #rg#ty #n  6: #tl #ty'2907  7: #id #fl  8: #id #fl  9: # rg #id ]2901 [ 2: #sz #sg  3: #fl  4: #ty'  5: #ty #n  6: #tl #ty' 2902  7: #id #fl  8: #id #fl  9: #id ] 2908 2903 #H destruct (H) 2909 2904 %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
Note: See TracChangeset
for help on using the changeset viewer.