Changeset 1395 for src/common/GenMem.ma

Timestamp:

Oct 17, 2011, 5:41:44 PM (10 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:

• src/common/GenMem.ma (modified) (2 diffs)

src/common/GenMem.ma

@@ -126 +126 @@
 qed.
 
-definition alloc : ∀content. mem content → Z → Z → region → mem content × block ≝
+definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r ≝
   λcontent,m,lo,hi,r.
   let b ≝ mk_block r (nextblock … m) in
@@ -136 +136 @@
     (succ_nextblock_pos … m),
     b〉.
+% qed.
 
 (* Freeing a block.  Return the updated memory state where the given