Changeset 409 for Deliverables


Ignore:
Timestamp:
Dec 13, 2010, 3:58:29 PM (9 years ago)
Author:
campbell
Message:

Update a couple of examples; put support for animation in its own file.

Location:
Deliverables/D3.1/C-semantics
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/depends

    r401 r409  
    1414Cexec.ma Csem.ma IOMonad.ma Plogic/russell_support.ma extralib.ma
    1515binary/Z.ma arithmetics/compare.ma binary/positive.ma
     16Animation.ma Cexec.ma
    1617CexecComplete.ma Cexec.ma Plogic/connectives.ma
    1718Globalenvs.ma AST.ma Errors.ma Mem.ma Values.ma
  • Deliverables/D3.1/C-semantics/test/memorymodel.ma

    r12 r409  
    2121   store. *)
    2222ndefinition store0 := empty.
    23 ndefinition store1block : mem × block ≝ alloc store0 0 4.
     23ndefinition store1block : mem × block ≝ alloc store0 0 4 Any.
    2424ndefinition store1 : mem ≝ fst ?? store1block.
    2525ndefinition block := snd ?? store1block.
     
    2727(* write a value *)
    2828ndefinition store2 : mem.
    29   nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));
     29  nletin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
    3030
    3131  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
     
    3434(* overwrite the first byte of the value *)
    3535ndefinition store3 : mem.
    36   nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));
     36  nletin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
    3737
    3838  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
     
    4040 
    4141(* The size checking rejects the read and gives us Some Vundef. *)
    42 nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed.
     42nremark vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. //; nqed.
    4343
    4444(* The read is successful and returns a signed version of the value. *)
    45 nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
     45nremark vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
    4646
    4747(* NB: Double frees are allowed by the memory model (although not necessarily
     
    5353   stack memory in the semantics. *)
    5454ndefinition storeA := empty.
    55 ndefinition storeBblkB := alloc storeA 0 4.
    56 ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8.
     55ndefinition storeBblkB := alloc storeA 0 4 Any.
     56ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
    5757ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
    5858ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)).
     
    6161(* Access to the "object representation" (as the C standard puts it) is not specified. *)
    6262ndefinition storeI := empty.
    63 ndefinition storeIIblk := alloc storeA 0 4.
     63ndefinition storeIIblk := alloc storeA 0 4 Any.
    6464ndefinition storeIII : mem.
    65  nletin r ≝ (store Mint32 (fst ?? storeIIblk) (snd ?? storeIIblk) 0 (Vint one));
     65 nletin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
    6666  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
    6767  ##| #rr; #_; napply rr ##] nqed.
    68 ndefinition byte := load Mint8unsigned storeIII (snd ?? storeIIblk) 0.
     68ndefinition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
    6969nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)
  • Deliverables/D3.1/C-semantics/test/trivial.ma

    r9 r409  
    44include "Cexec.ma".
    55
    6 ndefinition main : ident ≝ O.
     6ndefinition main : ident ≝ succ_pos_of_nat O.
    77naxiom ident_eq_eq: ∀i. ident_eq i i = inl ?? (refl ? i).
    88
Note: See TracChangeset for help on using the changeset viewer.