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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.