Changeset 1395 for src/common/GenMem.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/common/GenMem.ma

    r1213 r1395  
    126126qed.
    127127
    128 definition alloc : ∀content. mem content → Z → Z → region → mem content × block
     128definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r
    129129  λcontent,m,lo,hi,r.
    130130  let b ≝ mk_block r (nextblock … m) in
     
    136136    (succ_nextblock_pos … m),
    137137    b〉.
     138% qed.
    138139
    139140(* Freeing a block.  Return the updated memory state where the given
Note: See TracChangeset for help on using the changeset viewer.