Changeset 2176 for src/common/Globalenvs.ma
 Timestamp:
 Jul 12, 2012, 1:28:28 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r2117 r2176 82 82 addresses of the memory region in question  here there are no real 83 83 pointers, so use the real region. *) 84 let ptr ≝ mk_pointer ( block_region m b) b ?(mk_offset p) in84 let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset p) in 85 85 match id with 86 86 [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n) … … 89 89  Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n) 90 90  Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n) 91  Init_addrof r'symb ofs ⇒91  Init_addrof (*r'*) symb ofs ⇒ 92 92 match find_symbol … ge symb with 93 93 [ None ⇒ None ? 94  Some b' ⇒ 94  Some b' ⇒ (* 95 95 match pointer_compat_dec b' r' with 96 [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc(shift_offset ? zero_offset (repr I16 ofs))))97  inr _ ⇒ None ?98 ] 96 [ inl pc ⇒*) store (ASTptr (*r'*)) m ptr (Vptr (mk_pointer (*r'*) b' (*pc*) (shift_offset ? zero_offset (repr I16 ofs)))) 97 (* inr _ ⇒ None ? 98 ]*) 99 99 ] 100 100  Init_space n ⇒ Some ? m 101  Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r')101  Init_null (*r'*) ⇒ store (ASTptr (*r'*)) m ptr (Vnull (*r'*)) 102 102 ]. 103 cases b //104 qed. 103 (*cases b // 104 qed.*) 105 105 106 106 definition size_init_data : init_data → nat ≝ … … 112 112  Init_float64 _ ⇒ 8 113 113  Init_space n ⇒ max n 0 114  Init_null r ⇒ size_pointer r115  Init_addrof r _ _ ⇒ size_pointer r].114  Init_null (*r*) ⇒ size_pointer (*r*) 115  Init_addrof (*r*) _ _ ⇒ size_pointer (*r*)]. 116 116 117 117 let rec store_init_data_list (F:Type[0]) (ge:genv_t F) … … 230 230 lemma find_funct_find_funct_ptr : ∀F,ge,v,f. 231 231 find_funct F ge v = Some F f → 232 ∃ pty,b,c. v = Vptr (mk_pointer pty b czero_offset) ∧ find_funct_ptr F ge b = Some F f.232 ∃(*pty,*)b(*,c*). v = Vptr (mk_pointer (*pty*) b (*c*) zero_offset) ∧ find_funct_ptr F ge b = Some F f. 233 233 #F #ge * 234 234 [ #f #E normalize in E; destruct 235 235  #sz #i #f #E normalize in E; destruct 236 236  #f #fn #E normalize in E; destruct 237  #r#f #E normalize in E; destruct238  * #pty #b #c* #off #f #E whd in E:(??%?);237  (*#r*) #f #E normalize in E; destruct 238  * (*#pty*) #b (*#c*) * #off #f #E whd in E:(??%?); 239 239 cases off in E ⊢ %; [ 2,3: #x ] 240 240 #E whd in E:(??%?); destruct 241 %{pty} %{b} %{c}% // @E241 (*%{pty}*) %{b} (*%{c}*) % // @E 242 242 ] qed. 243 243 … … 510 510 ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'. 511 511 #A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P 512 cases b * * [ 2,3,5,6 ,8,9,11,12,14,15,17,18: #bp ]513 [ 12: *: #F whd in F:(??%?); destruct ]512 cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ] 513 [ 4: (*12:*)  *: #F whd in F:(??%?); destruct ] 514 514 >vars_irrelevant_to_find_funct_ptr 515 515 >vars_irrelevant_to_find_funct_ptr … … 656 656 #A #B #V #iV #tf #p #v #f #FF 657 657 cases (find_funct_find_funct_ptr ???? FF) 658 # r * #b * #pc* #E destruct #FFP658 #b * #E destruct #FFP 659 659 change with (find_funct_ptr ???) in ⊢ (??%?); 660 660 @(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *) … … 676 676 #A #B #ge #ge' #m #b #o #d #SYM 677 677 whd in ⊢ (??%%); 678 cases d #d' try @refl679 # id #n whd in ⊢ (??%%);678 cases d try #d' try @refl 679 #n whd in ⊢ (??%%); 680 680 whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl 681 681 qed.
Note: See TracChangeset
for help on using the changeset viewer.