Changeset 2895 for src/RTLabs/RTLabs_abstract.ma
 Timestamp:
 Mar 16, 2013, 9:08:19 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabs_abstract.ma
r2757 r2895 35 35 match state with 36 36 [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack 37  Callstate _fd _ _ fs _ ⇒37  Callstate fid fd _ _ fs _ ⇒ 38 38 match fn_stack with 39 39 [ nil ⇒ False 40  cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧ 41 All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t 40  cons h t ⇒ 41 find_symbol … ge fid = Some ? h ∧ 42 find_funct_ptr ? ge h = Some ? fd ∧ 43 All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t 42 44 ] 43 45  Returnstate _ _ fs _ ⇒ … … 69 71  #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct 70 72 whd cases stk in mtc ⊢ %; [ * ] 71 #hd #tl #H @H73 #hd #tl * * /3/ 72 74  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct 73 75  #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct … … 76 78  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct 77 79 ] 78  s' # vf#fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP80  s' #fid #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP 79 81 whd % // func_block cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX) 80 82 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct … … 232 234 match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with 233 235 [ mk_RTLabs_ext_state s' stk mtc0 ⇒ 234 match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with 235 [ Callstate _ fd _ _ _ _ ⇒ 236 match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with 237 [ nil ⇒ λmtc. ⊥ 238  cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ? 239 ] 240  State f _ _ ⇒ λ_. λH.⊥ 241  _ ⇒ λ_. λH.⊥ 242 ] mtc0 236 match s' return λs'. RTLabs_classify s' = cl_call → ident with 237 [ Callstate fid _ _ _ _ _ ⇒ λ_. fid 238  State f _ _ ⇒ λH.⊥ 239  _ ⇒ λH.⊥ 240 ] 243 241 ] p 244 242 ]. … … 246 244 cases (next_instruction f) in H; 247 245 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct 248  4,5: normalize in H; destruct (H) 249  cases mtc 250  cases mtc #FFP #_ >FFP % #E destruct (E) 246  *: normalize in H; destruct (H) 251 247 ] qed. 252 248
Note: See TracChangeset
for help on using the changeset viewer.