Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/memorymodel.ma

    r717 r961  
    2727(* write a value *)
    2828definition store2 : mem.
    29   letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));
     29  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));
    3030
    3131  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     
    3434(* overwrite the first byte of the value *)
    3535definition store3 : mem.
    36   letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));
     36  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
    3737
    3838  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
     
    4242example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.
    4343
    44 (* The read is successful and returns a signed version of the value. *)
    45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed.
     44(* The read is successful and returns the value. *)
     45example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed.
    4646
    4747(* NB: Double frees are allowed by the memory model (although not necessarily
     
    6363definition storeIIblk := alloc storeA 0 4 Any.
    6464definition storeIII : mem.
    65  letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));
     65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
    6666  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
    6767  | #rr #_ @rr ] qed.
Note: See TracChangeset for help on using the changeset viewer.