ACSL Language Reference (811287), страница 18
Текст из файла (страница 18)
ILLUSTRATIVE EXAMPLE133134135136@ predicate chunk_lower_length(memory_chunk_list* ptr1,@memory_chunk_list* ptr2) =@ lower_length(next_chunk, ptr1, ptr2) ;@*/137138139140141142143144145146147/* A memory slice holds together a memory block [block] and a list of chunks* [chunks] on this memory block.*/typedef struct _memory_slice {//@ ghost booleanpacked;// ghost field [packed] is meant to be used as a guard that tells when// the invariant of a structure of type [memory_slice] holdsmemory_block*block;memory_chunk_list* chunks;} memory_slice;148149150151152153154155156157/*@ strong type invariant inv_memory_slice(memory_slice* ms) =@ ms.packed ==>@(valid_memory_block(ms->block) && ms->block->slice == ms@&& (ms->chunks == \null@|| valid_complete_chunk_list(ms->chunks, ms->block))) ;@@ predicate valid_memory_slice(memory_slice* ms) =@\valid (ms) && ms->packed ;@*/158159160161162163164165166167168169/* A memory slice list links memory slices, to form a memory pool.*/typedef struct _memory_slice_list {//@ ghost booleanpacked;// ghost field [packed] is meant to be used as a guard that tells when// the invariant of a structure of type [memory_slice_list] holdsmemory_slice*slice;// current list elementstruct _memory_slice_list* next;// tail of the list} memory_slice_list;170171172173174175176177178179180181182183184185186187/*@@@@@@@@@@@@@@@@@logic memory_slice_list* next_slice(memory_slice_list* ptr) =ptr->next ;strong type invariant inv_memory_slice_list(memory_slice_list* msl) =msl.packed ==>(valid_memory_slice(msl->slice)&& (msl->next == \null ||valid_memory_slice_list(msl->next))&& finite_list(next_slice, msl)) ;predicate valid_memory_slice_list(memory_slice_list* msl) =\valid (msl) && msl->packed ;predicate slice_lower_length(memory_slice_list* ptr1,memory_slice_list* ptr2) =lower_length(next_slice, ptr1, ptr2)} */18897APPENDIX A.
APPENDICES189typedef memory_slice_list* memory_pool;190191192193/*@ type invariant valid_memory_pool(memory_pool *mp) =@\valid (mp) && valid_memory_slice_list(*mp) ;@*/194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244/*@ behavior zero_size:@ assumes s == 0;@assigns \nothing;@ensures \result == 0;@@ behavior positive_size:@ assumes s > 0;@requires valid_memory_pool(arena);@ensures \result == 0@|| (valid_memory_chunk(\result,s) &&@used_memory_chunk(*\result));@ */memory_chunk* memory_alloc(memory_pool* arena, unsigned int s) {memory_slice_list *msl = *arena;memory_chunk_list *mcl;memory_slice *ms;memory_block *mb;memory_chunk *mc;unsigned int mb_size;//@ ghost unsigned int mcl_offset;char *mb_data;// guard conditionif (s == 0) return 0;// iterate through memory blocks (or slices)/*@@ loop invariant valid_memory_slice_list(msl);@ loop variant msl for slice_lower_length;@ */while (msl != 0) {ms = msl->slice;mb = ms->block;mcl = ms->chunks;// does [mb] contain enough free space?if (s <= mb->size - mb->next) {//@ ghost ms->ghost = false; // unpack the slice// allocate a new chunkmc = (memory_chunk*)malloc(sizeof(memory_chunk));if (mc == 0) return 0;mc->offset = mb->next;mc->size = s;mc->free = false;mc->block = mb;//@ ghost mc->ghost = true; // pack the chunk// update block accordingly//@ ghost mb->ghost = false; // unpack the blockmb->next += s;mb->used += s;//@ ghost mb->ghost = true; // pack the block// add the new chunk to the listmcl = (memory_chunk_list*)malloc(sizeof(memory_chunk_list));98A.5.
ILLUSTRATIVE EXAMPLE245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300if (mcl == 0) return 0;mcl->chunk = mc;mcl->next = ms->chunks;ms->chunks = mcl;//@ ghost ms->ghost = true; // pack the slicereturn mc;}// iterate through memory chunks/*@@ loop invariant valid_memory_chunk_list(mcl,mb);@ loop variant mcl for chunk_lower_length;@ */while (mcl != 0) {mc = mcl->chunk;// is [mc] free and large enough?if (mc->free && s <= mc->size) {mc->free = false;mb->used += mc->size;return mc;}// try next chunkmcl = mcl->next;}msl = msl->next;}// allocate a new blockmb_size = (DEFAULT_BLOCK_SIZE < s) ? s : DEFAULT_BLOCK_SIZE;mb_data = (char*)malloc(mb_size);if (mb_data == 0) return 0;mb = (memory_block*)malloc(sizeof(memory_block));if (mb == 0) return 0;mb->size = mb_size;mb->next = s;mb->used = s;mb->data = mb_data;//@ ghost mb->ghost = true; // pack the block// allocate a new chunkmc = (memory_chunk*)malloc(sizeof(memory_chunk));if (mc == 0) return 0;mc->offset = 0;mc->size = s;mc->free = false;mc->block = mb;//@ ghost mc->ghost = true; // pack the chunk// allocate a new chunk listmcl = (memory_chunk_list*)malloc(sizeof(memory_chunk_list));if (mcl == 0) return 0;//@ ghost mcl->offset = 0;mcl->chunk = mc;mcl->next = 0;// allocate a new slicems = (memory_slice*)malloc(sizeof(memory_slice));if (ms == 0) return 0;ms->block = mb;ms->chunks = mcl;//@ ghost ms->ghost = true; // pack the slice99APPENDIX A.
APPENDICES301302303304305306307308309310311}// update the block accordinglymb->slice = ms;// add the new slice to the listmsl = (memory_slice_list*)malloc(sizeof(memory_slice_list));if (msl == 0) return 0;msl->slice = ms;msl->next = *arena;//@ ghost msl->ghost = true; // pack the slice list*arena = msl;return mc;312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356/*@ behavior null_chunk:@ assumes chunk == \null;@assigns \nothing;@@ behavior valid_chunk:@ assumes chunk != \null;@requires valid_memory_pool(arena);@requires valid_memory_chunk(chunk,chunk->size);@requires used_memory_chunk(chunk);@ensures@// if it is not the last chunk in the block, mark it as free@(valid_memory_chunk(chunk,chunk->size)@&& freed_memory_chunk(chunk))@||@// if it is the last chunk in the block, deallocate the block@! \valid (chunk);@ */void memory_free(memory_pool* arena, memory_chunk* chunk) {memory_slice_list *msl = *arena;memory_block *mb = chunk->block;memory_slice *ms = mb->slice;memory_chunk_list *mcl;memory_chunk *mc;// is it the last chunk in use in the block?if (mb->used == chunk->size) {// remove the corresponding slice from the memory pool// case it is the first sliceif (msl->slice == ms) {*arena = msl->next;//@ ghost msl->ghost = false; // unpack the slice listfree(msl);}// case it is not the first slicewhile (msl != 0) {if (msl->next != 0 && msl->next->slice == ms) {memory_slice_list* msl_next = msl->next;msl->next = msl->next->next;// unpack the slice list//@ ghost msl_next->ghost = false;free(msl_next);break;}msl = msl->next;}100A.6.
CHANGES//@ ghost ms->ghost = false; // unpack the slice// deallocate all chunks in the blockmcl = ms->chunks;// iterate through memory chunks/*@@ loop invariant valid_memory_chunk_list(mcl,mb);@ loop variant mcl for chunk_lower_length;@ */while (mcl != 0) {memory_chunk_list *mcl_next = mcl->next;mc = mcl->chunk;//@ ghost mc->ghost = false; // unpack the chunkfree(mc);free(mcl);mcl = mcl_next;}mb->next = 0;mb->used = 0;// deallocate the memory block and its data//@ ghost mb->ghost = false;// unpack the blockfree(mb->data);free(mb);// deallocate the corresponding slicefree(ms);return ;357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388}A.6A.6.1}// mark the chunk as freedchunk->free = true;// update the block accordinglymb->used -= chunk->size;return ;ChangesVersion 1.12• Fixes syntax rule for statement contracts in allowing completeness clauses (figure 2.12)A.6.2Version 1.11• Functions related to infinites and the sign of floating-point value (section 2.2.5)• New section for predicates related to well-typedness (section 2.14)• Syntax for defining a set by giving explicitely its elements (section 2.3.4)• Adding lists as first-class values (section 2.8.2)• Change the associativity of bitwise operator --> to right, in accordance with the one of==> operator• Glyph used for ^^ operator (xor) fixed101APPENDIX A.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
