Changeset 1395 for src/common


Ignore:
Timestamp:
Oct 17, 2011, 5:41:44 PM (9 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.

Location:
src/common
Files:
2 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
  • src/common/Globalenvs.ma

    r1231 r1395  
    390390definition empty_mem ≝ empty. (* XXX*)
    391391definition empty : ∀F. genv F ≝
    392   λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?).
    393 (*  mkgenv (ZMap.init None) (-1) (PTree.empty block).*)
     392  λF. mk_genv F (λ_. None ?) (-2) (λ_. None ?).
     393(*  mkgenv (ZMap.init None) (-2) (PTree.empty block).*)
    394394
    395395definition add_functs : ∀F:Type[0]. genv F → list (ident × F) → genv F ≝
Note: See TracChangeset for help on using the changeset viewer.