Changeset 2332 for src/common


Ignore:
Timestamp:
Sep 12, 2012, 12:36:46 PM (7 years ago)
Author:
garnier
Message:

Some progress on switch removal. Small fix in the definition of free, in GenMem?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r2185 r2332  
    134134  address will fail.  Note that we make no attempt to return the block
    135135  to an allocation pool: the given block address will never be allocated
    136   later. *)
     136  later. We make sure that no valid_pointer can exist towards this block. *)
    137137
    138138definition free ≝
    139139  λm,b.mk_mem (update_block … b
    140               (empty_block … OZ OZ)
     140              (empty_block … (pos one) OZ)
    141141              (blocks … m))
    142142        (nextblock … m)
Note: See TracChangeset for help on using the changeset viewer.