Changeset 2468 for src/Clight/CexecSound.ma
 Timestamp:
 Nov 15, 2012, 6:12:57 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r2428 r2468 5 5 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). 6 6 #v #ty #r 7 cases v; [  #sz #i  #f   #ptr ] 8 cases ty; [ 2,11,20,29,38: #sz' #sg  3,12,21,30,39: #sz'  4,13,22,31,40: (*#rg*) #ty  5,14,23,32,41: (*#r*) #ty #n  6,15,24,33,42: #args #rty  7,8,16,17,25,26,34,35,43,44: #id #fs  9,18,27,36,45: (*#r*) #id ] 7 cases v; [  #sz #i (* #f*)   #ptr ] 8 cases ty; [ 2,10,18,26: #sz' #sg  3,11,19,27: #ty'  4,12,20,28: (*#r*) #ty #n 9  5,13,21,29: #args #rty  6,7,14,15,22,23,30,31: #id #fs  8,16,24,32: (*#r*) #id ] 9 10 whd in ⊢ (??%? → ?); 10 11 [ 2: @intsize_eq_elim_elim … … 15 16 ] 16 17 ] 17  8: #H cases (eq_dec f Fzero)18 (* 8: #H cases (eq_dec f Fzero) 18 19 [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float 19 20  #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne 20 ] 21  14: #H destruct @bool_of_val_false @is_false_pointer22  15: #H destruct @bool_of_val_true @is_true_pointer_pointer21 ]*) 22  7: #H destruct @bool_of_val_false @is_false_pointer 23  8: #H destruct @bool_of_val_true @is_true_pointer_pointer 23 24  *: #H destruct 24 25 ] qed. … … 39 40 @eq_bv_elim 40 41 [ #e >e 41 cases ty; [  #sz' #sg  #fs (*#sp*) #ty  (*#sp*) #ty #n  #args #rty  #id #fs  #id #fs  (*#r*) #id ]42 cases ty; [  #sz' #sg (*  #fs *)  (*#sp*) #ty  (*#sp*) #ty #n  #args #rty  #id #fs  #id #fs  (*#r*) #id ] 42 43 whd in ⊢ (??%? → ?); #H [ 2:  *: destruct ] 43 cases ty' in H ⊢ %; [  #sz'' #sg  #fs (*#sp*) #ty  (*#sp*) #ty #n  #args #rty  #id #fs  #id #fs  (*#r*) #id ]44 cases ty' in H ⊢ %; [  #sz'' #sg (*  #fs*)  (*#sp*) #ty  (*#sp*) #ty #n  #args #rty  #id #fs  #id #fs  (*#r*) #id ] 44 45 try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z // 45 46  #_ whd in ⊢ (??%? → ?); #H destruct 46 47 ] 47 qed. 48 qed. 48 49 49 50 lemma exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'. … … 53 54  #sz #i cases ty; 54 55 [ #H whd in H:(??%?); destruct; 55  3: #a #H whd in H:(??%?); destruct; 56  7,8,9: #a [ 1,2: #b ] #H whd in H:(??%?); destruct;56 (*  3: #a #H whd in H:(??%?); destruct; *) 57  6,7,8: #a [ 1,2: #b ] #H whd in H:(??%?); destruct; 57 58  #sz1 #si1 cases ty'; 58 59 [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim … … 60 61  *; whd #H whd in H:(??%?); destruct; 61 62 ] 62  3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim63 (*  3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 63 64 [ #E #H whd in H:(??%?); destruct 64 65  *; whd #H whd in H:(??%?); destruct; @cast_if 65 ] 66  2, 7,8,9: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim66 ] *) 67  2,6,7,8: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim 67 68 [ 1,3,5,7: #NE #H destruct 68 69  *: *; whd #H whd in H:(??%?); destruct; // 69 70 ] 70  4,5,6: [ #ty'' letin t ≝ (Tpointer ty'')71  3,4,5: [ #ty'' letin t ≝ (Tpointer ty'') 71 72  #ty'' #n letin t ≝ (Tarray ty'' n) 72 73  #args #rty letin t ≝ (Tfunction args rty) ] … … 91 92 ] 92 93 ] 93  #f cases ty; [ 3,4,9: #x  2,5,6,7,8: #x #y ]94 (* #f cases ty; [ 3,4,9: #x  2,5,6,7,8: #x #y ] 94 95 [ cases ty'; [ #e  3,4,9: #a #e  2,6,7,8: #a #b #e  #a #b #e ] 95 96 whd in e:(??%?); destruct; //; 96 97  *: #e whd in e:(??%?); destruct 97 ] 98  cases ty; [ 3, 4,9: #x  2,5,6,7,8: #x #y ]98 ] *) 99  cases ty; [ 3,8: #x  2,4,5,6,7: #x #y ] 99 100 whd in ⊢ (??%? → ?); #H destruct 100 101 cases ty' in H; normalize; try #a try #b try #c try #d destruct; … … 121 122 *) 122 123  #ptr 123 cases ty; [ 3,4,9: #x  2,5,6,7,8: #x #y ]124 cases ty; [ 3,8: #x  2,4,5,6,7: #x #y ] 124 125 #E whd in E:(??%?); destruct 125 126 cases ty' in E ⊢ %; normalize #A try #B try #C try #D destruct /2/ 126 127 ] qed. 128 129 127 130 128 131 … … 132 135 [ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%); 133 136 @eq_intsize_elim #E try @I <E whd % 134  #ty #c whd // 137 (* #ty #c whd //*) 135 138 (* expressions that are lvalues *) 136 139  #e' #ty cases e'; //; [ #i #He'  #e #He'  #e #i #He' ] whd in He' ⊢ %; … … 210 213 (* exec_lvalue fails on nonlvalues. *) 211 214  #e' #ty cases e'; 212 [ 2, 5,12: #a #H  3,4: #a *  13,14: #a #b *  1,6,8,10,11: #a #b #H  7,9: #a #b #c #H]213 @I215 [ 2,4,11: #a #H try @I @(False_ind … H)  3: #a *  12,13: #a #b *  1,5,7,9,10: #a #b #H @I  6,8: #a #b #c #H @I ] 216 try @I 214 217 ] qed. 215 218 … … 218 221 eval_lvalue ge en m e loc off tr. 219 222 #ge #en #m #e #loc #off #tr #ty #H inversion H; 220 [ 1, 2,5: #a #b #c #H @False_ind destruct (H);223 [ 1,4: #a #b #c #H @False_ind destruct (H); 221 224  #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind 222 225 @(eval_lvalue_inv_ind … H1) … … 318 321 [ // 319 322  #ty #tys whd in ⊢ (???%); 320 cases ty [ #sz #sg   #sz] cases v //321 [#sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);322 @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct323  #v ]@bind_OK #evs #CHECKevs323 cases ty [ #sz #sg  ] cases v // 324 #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?); 325 @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct 326 @bind_OK #evs #CHECKevs 324 327 @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs)) 325 328 //
Note: See TracChangeset
for help on using the changeset viewer.