Changeset 1395 for src/joint/BEMem.ma


Ignore:
Timestamp:
Oct 17, 2011, 5:41:44 PM (8 years ago)
Author:
sacerdot
Message:

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

end of program execution. Differently from what happens in OCaml, the block
is not allocated.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r1329 r1395  
    2929definition pointer_of_address: address → res pointer ≝
    3030 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
     31definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
    3132
    32 (*CSC: for pointers of type Code and XData, the next function type can be
    33  strengthtened to never fail *)
    34 definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
     33definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
     34definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
    3535
    3636definition addr_add: address → nat → res address ≝
    3737 λaddr,n.
    38   do ptr ← pointer_of_address addr ;
    39   address_of_pointer (shift_pointer 16 ptr (bitvector_of_nat … n)).
     38  do ptr ← code_pointer_of_address addr ;
     39  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
     40normalize cases ptr #p #E @E
     41qed.
    4042
    4143definition addr_sub: address → nat → res address ≝
    4244 λaddr,n.
    43   do ptr ← pointer_of_address addr ;
    44   address_of_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n)).
     45  do ptr ← code_pointer_of_address addr ;
     46  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
     47normalize cases ptr #p #E @E
     48qed.
Note: See TracChangeset for help on using the changeset viewer.