Changeset 2638
 Timestamp:
 Feb 7, 2013, 2:15:51 PM (8 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLtoERTLptrOK.ma
r2604 r2638 1279 1279 fetch_function … (globalenv (λvars.fundef (F vars)) V i p) 1280 1280 bl = Error … [MSG BadFunction]. 1281 #F#V#i#p ** #r #id #EQ1 #EQ2destruct1281 #F#V#i#p ** #r #id #EQ1 destruct 1282 1282 whd in match fetch_function; normalize nodelta 1283 1283 >globalenv_no_minus_one … … 1290 1290 fetch_function … (globalenv (λvars.fundef (F vars)) V i p) 1291 1291 bl = Error … [MSG BadFunction]. 1292 #F#V#i#p ** #r #id #EQ1 #EQ2destruct1292 #F#V#i#p ** #r #id #EQ1 destruct 1293 1293 whd in match fetch_function; normalize nodelta 1294 1294 >globalenv_no_zero 
src/joint/Traces.ma
r2601 r2638 74 74 let sem_globals : evaluation_params ≝ pars in 75 75 let ge ≝ ev_genv sem_globals in 76 let m ≝ alloc_mem … p in77 let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XDatain76 let m0 ≝ alloc_mem … p in 77 let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in 78 78 let spp : xpointer ≝ 79 79 «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)), … … 95 95  External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) 96 96 ]. 97 cases m0 in H; #m1 #m2 #m3 #H 98 whd in H:(???%); destruct whd in ⊢(??%?); @Zltb_elim_Type0 // #abs @⊥ 99 @(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by transitive_Zlt/ 100 qed. 97 101 98 102 definition joint_classify_step : 
src/joint/joint_semantics.ma
r2601 r2638 75 75 (* special program counter that is guaranteed to not correspond to anything *) 76 76 definition exit_pc : program_counter ≝ 77 mk_program_counter «mk_block Code(1), refl …» one.77 mk_program_counter «mk_block (1), refl …» one. 78 78 79 79 definition null_pc : Pos → program_counter ≝ λpos. 80 mk_program_counter «mk_block Code OZ, refl …» pos. 80 mk_program_counter «mk_block ?, ?» pos. 81 cases daemon qed. 81 82 82 83 definition set_m: ∀p. bemem → state p → state p ≝ … … 161 162 fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p) 162 163 bl = Error … [MSG BadFunction]. 163 #F#V#i#p ** #r #id #EQ1 #EQ2destruct164 #F#V#i#p ** #r #id #EQ1 destruct 164 165 whd in match fetch_internal_function; 165 166 whd in match fetch_function; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.