Changeset 485
- Timestamp:
- Feb 2, 2011, 12:41:05 PM (10 years ago)
- Location:
- Deliverables/D3.1/C-semantics
- Files:
-
- 1 added
- 10 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.1/C-semantics/AST.ma
r483 r485 147 147 | Init_space: Z → init_data 148 148 | Init_null: region → init_data 149 | Init_addrof: ident → int → init_data (*r address of symbol + offset *) 150 | Init_pointer: list init_data → init_data. 149 | Init_addrof: region → ident → int → init_data. (*r address of symbol + offset *) 151 150 152 151 (* * Whole programs consist of: -
Deliverables/D3.1/C-semantics/Cexec.ma
r484 r485 98 98 #A B C P P' e f; nelim e; //; 99 99 #v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed. 100 101 ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].102 nlemma opt_OK: ∀A,P,e.103 (∀v. e = Some ? v → P v) →104 match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].105 #A P e; nelim e; /2/;106 nqed.107 100 108 101 nlemma opt_bind_OK: ∀A,B,P,e,f. … … 679 672 ]. 680 673 681 nlet rec make_initial_state (p:clight_program) : res state≝682 let ge ≝ globalenv Genv ?? p in683 let m0 ≝ init_mem Genv ?? p in684 685 686 687 OK ? (Callstate f (nil ?) Kstop m0).674 nlet rec make_initial_state (p:clight_program) : res (genv × state) ≝ 675 do ge ← globalenv Genv ?? p; 676 do m0 ← init_mem Genv ?? p; 677 do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p)); 678 do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]); 679 do f ← opt_to_res ? (find_funct_ptr ? ? ge b); 680 OK ? 〈ge,Callstate f (nil ?) Kstop m0〉. 688 681 689 682 ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r). … … 756 749 757 750 ndefinition exec_inf : clight_program → execution ≝ 758 λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉). 751 λp. 752 match make_initial_state p with 753 [ OK gs ⇒ exec_inf_aux (\fst gs) (ret ? 〈E0,\snd gs〉) 754 | _ ⇒ e_wrong 755 ]. 759 756 760 757 nremark execution_cases: ∀e. -
Deliverables/D3.1/C-semantics/CexecComplete.ma
r484 r485 57 57 initial_state p s → initial_state p s' → s = s'. 58 58 #p s s' H1 H2; 59 ninversion H1; #b1 f1 e11 e12 e13; 60 ninversion H2; #b2 f2 e21 e22 e23; 61 nrewrite > e11 in e21; 62 #e1; nrewrite > (?:b1 = b2) in e12; 63 ##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1); 59 ninversion H1; #b1 f1 ge1 m1 e11 e12 e13 e14 e15; 60 ninversion H2; #b2 f2 ge2 m2 e21 e22 e23 e24 e25; 61 nrewrite > e11 in e21; #e1; nrewrite > (?:ge1 = ge2) in e13 e14; 62 ##[ ##2: ndestruct (e1) skip (e11); napply refl; ##] 63 #e13 e14; 64 65 nrewrite > e12 in e22; #e2; ndestruct (e2) skip (e12); 66 67 nrewrite > e13 in e23; #e3; nrewrite > (?:b1 = b2) in e14; 68 ##[ nrewrite > e24; #e4; nrewrite > (?:f2 = f1); 64 69 ##[ //; 65 ##| ndestruct (e 2) skip (e22 e23); //;70 ##| ndestruct (e4) skip (e24 e25); //; 66 71 ##] 67 ##| ndestruct (e 1) skip (e11); //72 ##| ndestruct (e3) skip (e13); // 68 73 ##] nqed. 69 74 … … 78 83 79 84 ntheorem the_initial_state: 80 ∀p,s. initial_state p s → yields ? (make_initial_state p) s.85 ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉. 81 86 #p s; ncases p; #fns main globs H; 82 87 ninversion H; 83 #b f e1 e2 e3;88 #b f ge m e1 e2 e3 e4 e5; @ge; 84 89 nwhd in ⊢ (??%?); 85 90 nrewrite > e1; 86 91 nwhd in ⊢ (??%?); 87 92 nrewrite > e2; 93 nwhd in ⊢ (??%?); 94 nrewrite > e3; 95 nwhd in ⊢ (??%?); 96 nrewrite > e4; 88 97 nwhd; napply refl; 89 98 nqed. -
Deliverables/D3.1/C-semantics/CexecEquiv.ma
r399 r485 948 948 ¬ ∃r.final_state s r. 949 949 #ge s H; ncases H; 950 #b f E1 E2; @; *; #r H2;950 #b f ge m E1 E2 E3 E4; @; *; #r H2; 951 951 ninversion H2; 952 #r' m E3 E4; ndestruct (E3);952 #r' m' E5 E6; ndestruct (E5); 953 953 nqed. 954 954 … … 972 972 ∃b.execution_matches_behavior e b ∧ exec_program p b. 973 973 #classic constructive_indefinite_description p e; 974 nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);974 nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); 975 975 nlapply (make_initial_state_sound p); 976 976 nlapply (the_initial_state p); 977 977 ncases (make_initial_state p); 978 ##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?(??%)? → ?); 978 ##[ #gs; ncases gs; #ge s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?%? → ?); 979 ncases INITIAL; #Ege INITIAL''; 979 980 nrewrite > (exec_inf_aux_unfold …); 980 981 nwhd in ⊢ (?%? → ?); 981 982 ncases (is_final_state s); 982 983 ##[ #F; napply False_ind; 983 napply (absurd ?? (initial_state_not_final … INITIAL ));984 napply (absurd ?? (initial_state_not_final … INITIAL'')); 984 985 ncases F; #r F'; @r; napply F'; 985 986 ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e; … … 989 990 (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC')); 990 991 *; #b MATCHES; @b; @; //; 992 #ge'; nrewrite > Ege; #Ege'; nrewrite > (?:ge' = ge); ##[ ##2: ndestruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ##] 991 993 ninversion MATCHES; 992 994 ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM; … … 995 997 nrewrite > E1 in TERM; #TERM; 996 998 napply (program_terminates (mk_transrel … step) ?? ge s); 997 ##[ ##2: napply INITIAL 999 ##[ ##2: napply INITIAL'' 998 1000 ##| ##3: napply (terminates_sound … TERM EXEC'); 999 1001 ##| ##skip … … 1008 1010 #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS; 1009 1011 ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV; 1010 napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);1012 napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR); 1011 1013 napply (silent_sound … DIVERGING EXECDIV); 1012 1014 ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS; … … 1017 1019 ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##] 1018 1020 #E7; nrewrite < E7 in REACTING; #REACTING; 1019 napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL );1021 napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL''); 1020 1022 napply (reacts_sound … REACTING EXEC'); 1021 1023 ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG; … … 1024 1026 ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7; 1025 1027 nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG; 1026 ncut (e0 = e''); ##[ ndestruct (E6) skip ( MATCHES EXEC0 EXEC'); // ##]1028 ncut (e0 = e''); ##[ ndestruct (E6) skip (INITIAL MATCHES EXEC0 EXEC'); // ##] 1027 1029 #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG; 1028 1030 nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL; 1029 napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);1031 napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP); 1030 1032 #r; @; #F; napply (absurd ?? FINAL); @r; napply F; 1031 1033 ##| #E; ndestruct (E); … … 1035 1037 #NOINIT; #_; #EXEC; 1036 1038 @ (Goes_wrong E0); @; 1037 ##[ nwhd in EXEC:(?(??%)?); 1038 nrewrite > (exec_inf_aux_unfold …) in EXEC; nwhd in ⊢ (?%? → ?); 1039 ncases e; 1039 ##[ nwhd in EXEC:(?%?); 1040 ncases e in EXEC; 1040 1041 ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##] 1041 1042 ncases (se_inv … EXEC0); 1042 1043 napply emb_initially_wrong; 1043 ##| napply program_goes_initially_wrong; 1044 #s; @; napply NOINIT; 1045 ##] 1046 ##] nqed. 1047 1044 ##| #ge Ege; 1045 napply program_goes_initially_wrong; 1046 #s; @; #INIT; ncases (NOINIT s INIT); #ge' H; napply H; 1047 ##] 1048 ##] nqed. 1049 -
Deliverables/D3.1/C-semantics/CexecSound.ma
r484 r485 1 1 include "Cexec.ma". 2 3 include "Plogic/connectives.ma". 2 4 3 5 nlemma exec_bool_of_val_sound: ∀v,ty,r. … … 455 457 nqed. 456 458 457 nlemma make_initial_state_sound : ∀p. P_res ? (λ s.initial_state p s) (make_initial_state p).459 nlemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p). 458 460 #p; ncases p; #fns main vars; 459 461 nwhd in ⊢ (???%); 462 napply bind_OK; #ge Ege; 463 napply bind_OK; #m Em; 460 464 napply opt_bind_OK; #x; ncases x; #sp b esb; 461 465 napply opt_bind_OK; #u ecode; 462 466 napply opt_bind_OK; #f ef; 463 467 ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##] 464 nwhd; napply (initial_state_intro …esb ef);468 nwhd; @; //; napply (initial_state_intro … Ege Em esb ef); 465 469 nqed. 466 470 -
Deliverables/D3.1/C-semantics/Csem.ma
r484 r485 1476 1476 1477 1477 ninductive initial_state (p: clight_program): state -> Prop := 1478 | initial_state_intro: ∀b,f .1479 let ge := globalenv Genv ?? p in1480 let m0 := init_mem Genv ?? p in1481 find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 ->1482 find_funct_ptr ?? ge b = Some ? f ->1478 | initial_state_intro: ∀b,f,ge,m0. 1479 globalenv Genv ?? p = OK ? ge → 1480 init_mem Genv ?? p = OK ? m0 → 1481 find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 → 1482 find_funct_ptr ?? ge b = Some ? f → 1483 1483 initial_state p (Callstate f (nil ?) Kstop m0). 1484 1484 … … 1495 1495 1496 1496 ndefinition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. 1497 program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh. 1497 ∀ge. globalenv ??? p = OK ? ge → 1498 program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. 1498 1499 (* 1499 1500 (** Big-step execution of a whole program. *) -
Deliverables/D3.1/C-semantics/Errors.ma
r250 r485 17 17 include "Plogic/equality.ma". 18 18 include "Plogic/connectives.ma". 19 include "datatypes/sums.ma". 19 20 20 21 (* * Error reporting and the error monad. *) … … 192 193 end. 193 194 *) 195 196 197 ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ]. 198 nlemma opt_OK: ∀A,P,e. 199 (∀v. e = Some ? v → P v) → 200 match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ]. 201 #A P e; nelim e; /2/; 202 nqed. -
Deliverables/D3.1/C-semantics/Globalenvs.ma
r480 r485 52 52 of function descriptions. *) 53 53 54 globalenv: ∀F,V: Type. program F V → genv_t F;54 globalenv: ∀F,V: Type. program F V → res (genv_t F); 55 55 (* * Return the global environment for the given program. *) 56 56 57 init_mem: ∀F,V: Type. program F V → mem;57 init_mem: ∀F,V: Type. program F V → res mem; 58 58 (* * Return the initial memory state for the given program. *) 59 59 … … 396 396 foldr ?? (add_funct F) init fns. 397 397 398 (* init *) 399 400 ndefinition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝ 401 λF,ge,m,r,b,p,id. 402 match id with 403 [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n) 404 | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n) 405 | Init_int32 n ⇒ store Mint32 m r b p (Vint n) 406 | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n) 407 | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n) 408 | Init_addrof r' symb ofs ⇒ 409 match (*find_symbol ge symb*) symbols ? ge symb with 410 [ None ⇒ None ? 411 | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' (snd ?? b') ofs) 412 ] 413 | Init_space n ⇒ Some ? m 414 | Init_null r' ⇒ store (Mpointer r') m r b p (Vnull r') 415 ]. 416 417 ndefinition size_init_data : init_data → Z ≝ 418 λi_data.match i_data with 419 [ Init_int8 _ ⇒ 1 420 | Init_int16 _ ⇒ 2 421 | Init_int32 _ ⇒ 4 422 | Init_float32 _ ⇒ 4 423 | Init_float64 _ ⇒ 8 424 | Init_space n ⇒ Zmax n 0 425 | Init_null r ⇒ size_pointer r 426 | Init_addrof r _ _ ⇒ size_pointer r]. 427 428 nlet rec store_init_data_list (F:Type) (ge:genv F) 429 (m: mem) (r: region) (b: block) (p: Z) (idl: list init_data) 430 on idl : option mem ≝ 431 match idl with 432 [ nil ⇒ Some ? m 433 | cons id idl' ⇒ 434 match store_init_data F ge m r b p id with 435 [ None ⇒ None ? 436 | Some m' ⇒ store_init_data_list F ge m' r b (p + size_init_data id) idl' 437 ] 438 ]. 439 440 ndefinition size_init_data_list : list init_data → Z ≝ 441 λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data. 442 443 (* Nonessential properties that may require arithmetic 444 nremark size_init_data_list_pos: 445 ∀i_data. OZ ≤ size_init_data_list i_data. 446 #i_data;nelim i_data;//; 447 #a;#tl;ncut (OZ ≤ size_init_data a) 448 ##[ncases a;nnormalize;//; 449 #x;ncases x;nnormalize;//; 450 ##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl)); 451 ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m) 452 ##[ncases (size_init_data a) in Hsize IH; 453 ##[##1,2:/3/ 454 ##|nnormalize;#n;#Hfalse;nelim Hfalse] 455 ##|#Hdisc;ncases Hdisc 456 ##[#Heq;nrewrite > Heq;//; 457 ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2; 458 (* TODO: arithmetics *) napply daemon] 459 ##] 460 ##] 461 nqed. 462 *) 463 464 ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝ 465 λm,i_data,bcl. 466 〈mk_mem (update ? (nextblock m) 467 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef) bcl) 468 (blocks m)) 469 (Zsucc (nextblock m)) 470 (succ_nextblock_pos m), 471 (nextblock m)〉. 472 473 (* init *) 474 398 475 ndefinition add_globals : ∀F,V:Type. 399 476 genv F × mem → list (ident × (list init_data) × region × V) → 400 genv F × mem≝401 λF,V,init ,vars.402 fold r??403 (λ id_init: ident × (list init_data) × region × V. λg_st: genv F × mem.477 res (genv F × mem) ≝ 478 λF,V,init_env,vars. 479 foldl ?? 480 (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V. 404 481 match id_init with [ mk_pair id_init1 info ⇒ 405 match id_init1 with [ mk_pair id_init2 bsp⇒482 match id_init1 with [ mk_pair id_init2 r ⇒ 406 483 match id_init2 with [ mk_pair id init ⇒ 407 match g_st with [ mk_pair g st ⇒ 408 match alloc_init_data st init bsp with [ mk_pair st' b ⇒ 409 〈add_symbol ? id bsp b g, st'〉 410 ] ] ] ] ]) 411 init vars. 412 413 ndefinition globalenv_initmem : ∀F,V:Type. program F V → genv F × mem ≝ 484 do 〈g,st〉 ← g_st; 485 match alloc_init_data st init r with [ mk_pair st' b ⇒ 486 let g' ≝ add_symbol ? id r b g in 487 do st'' ← opt_to_res ? (store_init_data_list F g' st' r b OZ init); 488 OK ? 〈g', st''〉 489 ] ] ] ]) 490 (OK ? init_env) vars. 491 492 ndefinition globalenv_initmem : ∀F,V:Type. program F V → res (genv F × mem) ≝ 414 493 λF,V,p. 415 494 add_globals F V 416 417 418 419 ndefinition globalenv_ : ∀F,V:Type. program F V → genv F≝495 〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉 496 (prog_vars ?? p). 497 498 ndefinition globalenv_ : ∀F,V:Type. program F V → res (genv F) ≝ 420 499 λF,V,p. 421 \fst (globalenv_initmem F V p). 422 ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝ 500 do 〈g,m〉 ← globalenv_initmem F V p; 501 OK ? g. 502 ndefinition init_mem_ : ∀F,V:Type. program F V → res (mem) ≝ 423 503 λF,V,p. 424 \snd (globalenv_initmem F V p). 504 do 〈g,m〉 ← globalenv_initmem F V p; 505 OK ? m. 506 507 508 425 509 426 510 ndefinition Genv : GENV ≝ mk_GENV … … 1304 1388 End Genv. 1305 1389 *) 1390 -
Deliverables/D3.1/C-semantics/Mem.ma
r484 r485 719 719 [ Vptr psp b ofs ⇒ store chunk m psp b (signed ofs) v 720 720 | _ ⇒ None ? ]. 721 722 723 (* Build a block filled with the given initialization data. *)724 ndefinition contents_init_data_step :725 Z → init_data → (Z → contentmap) → contentmap ≝726 λpos,data,reccall.727 match data with728 [ Init_int8 n ⇒729 setN 0 pos (Vint n) (reccall (pos + oneZ))730 | Init_int16 n ⇒731 setN 1 pos (Vint n) (reccall (pos + oneZ))732 | Init_int32 n ⇒733 setN 3 pos (Vint n) (reccall (pos + oneZ))734 | Init_float32 f ⇒735 setN 3 pos (Vfloat f) (reccall (pos + oneZ))736 | Init_float64 f ⇒737 setN 7 pos (Vfloat f) (reccall (pos + oneZ))738 | Init_space n ⇒ reccall (pos + Zmax n 0) (*??*)739 | Init_null r ⇒ setN (pred_size_pointer r) pos (Vnull r) (reccall (pos + oneZ))740 | Init_addrof s n ⇒741 (* Not handled properly yet *)742 reccall (pos + 4)743 | Init_pointer x ⇒744 (* Not handled properly yet *)745 reccall (pos + 4)].746 747 nlet rec contents_init_data (pos: Z) (i_data: list init_data) on i_data748 : contentmap ≝749 match i_data with750 [ nil ⇒ (λ_.Undef)751 | cons data i_data' ⇒752 contents_init_data_step pos data (λn.contents_init_data n i_data') ].753 754 ndefinition size_init_data : init_data → Z ≝755 λi_data.match i_data with756 [ Init_int8 _ ⇒ 1757 | Init_int16 _ ⇒ 2758 | Init_int32 _ ⇒ 4759 | Init_float32 _ ⇒ 4760 | Init_float64 _ ⇒ 8761 | Init_space n ⇒ Zmax n 0762 | Init_null r ⇒ size_pointer r763 | Init_addrof _ _ ⇒ 4764 | Init_pointer _ ⇒ Z_of_nat (*** can't use implicit coercion??? *)4].765 766 ndefinition size_init_data_list : list init_data → Z ≝767 λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.768 769 (* Nonessential properties that may require arithmetic770 nremark size_init_data_list_pos:771 ∀i_data. OZ ≤ size_init_data_list i_data.772 #i_data;nelim i_data;//;773 #a;#tl;ncut (OZ ≤ size_init_data a)774 ##[ncases a;nnormalize;//;775 #x;ncases x;nnormalize;//;776 ##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));777 ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)778 ##[ncases (size_init_data a) in Hsize IH;779 ##[##1,2:/3/780 ##|nnormalize;#n;#Hfalse;nelim Hfalse]781 ##|#Hdisc;ncases Hdisc782 ##[#Heq;nrewrite > Heq;//;783 ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;784 (* TODO: arithmetics *) napply daemon]785 ##]786 ##]787 nqed.788 *)789 790 ndefinition block_init_data : list init_data → region → block_contents ≝791 λi_data,bcl.mk_block_contents792 OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.793 794 ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝795 λm,i_data,bcl.796 〈mk_mem (update ? (nextblock m)797 (block_init_data i_data bcl)798 (blocks m))799 (Zsucc (nextblock m))800 (succ_nextblock_pos m),801 (nextblock m)〉.802 803 nremark block_init_data_empty:804 ∀bcl. block_init_data [ ] bcl = empty_block OZ OZ bcl.805 //;806 nqed.807 721 808 722 (* * Properties of the memory operations *) -
Deliverables/D3.1/C-semantics/test/insertsort.c
r479 r485 4 4 }; 5 5 6 /* Init_addrof not yet supported7 6 __pdata struct list l6 = {69, 0}; 8 7 __pdata struct list l5 = {36, &l6}; … … 12 11 __pdata struct list l1 = {240, &l2}; 13 12 __pdata struct list l0 = {102, &l1}; 14 */15 __pdata struct list l6 = {69, 0};16 __pdata struct list l5 = {36, 0};17 __pdata struct list l4 = {136, 0};18 __pdata struct list l3 = {105, 0};19 __pdata struct list l2 = {234, 0};20 __pdata struct list l1 = {240, 0};21 __pdata struct list l0 = {102, 0};22 13 23 14 void insert(__pdata struct list *element, __pdata struct list **dest) { … … 46 37 __pdata struct list *l = &l0; 47 38 48 /* Init_addrof not yet supported */49 l0.next = &l1;50 l1.next = &l2;51 l2.next = &l3;52 l3.next = &l4;53 l4.next = &l5;54 l5.next = &l6;55 56 39 sort(&l); 57 40 while (l) {
Note: See TracChangeset
for help on using the changeset viewer.