ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 16

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 16)

For instance, a function contract may need to refer to a globalvariable that has the same name as a function parameter, as in the following code:91APPENDIX A. APPENDICES123int x;//@ assigns x;int g();45678int f(int x) {// ...return g();}In order to write the assigns clause for f, we must access the global variable x, since f callsg, which can modify x. This is not possible with C scoping rules, as x refers to the parameterof f in the scope of the function.A solution is to use a ghost pointer to x, as shown in the following code:1int x;23//@ ghost int* const ghost_ptr_x = &x;456//@ assigns x;int g();789101112A.5//@ assigns *ghost_ptr_x;int f(int x) {// ...return g();}Illustrative exampleThis is an attempt to define an example for ACSL, much as the Purse example in JMLdescription papers. It is a memory allocator, whose main functions are memory_alloc andmemory_free, to respectively allocate and deallocate memory.

The goal is to exercise as muchas possible of ACSL.12#include <stdlib.h>34#define DEFAULT_BLOCK_SIZE 100056typedef enum _bool { false = 0, true = 1 } bool;7891011121314151617181920/*@ predicate finite_list<A>((A* -> A*) next_elem, A* ptr) =@ ptr == \null ||@ ( \valid (ptr) && finite_list(next_elem,next_elem(ptr))) ;@@ logic integer list_length<A>((A* -> A*) next_elem, A* ptr) =@ (ptr == \null) ? 0 :@ 1 + list_length(next_elem,next_elem(ptr)) ;@@@ predicate lower_length<A>((A* -> A*) next_elem,@A* ptr1, A* ptr2) =@ finite_list(next_elem, ptr1) && finite_list(next_elem, ptr2)@ && list_length(next_elem, ptr1) < list_length(next_elem, ptr2) ;92A.5.

ILLUSTRATIVE EXAMPLE21@*/222324// forward referencestruct _memory_slice;25262728293031323334353637383940414243444546/* A memory block holds a pointer to a raw block of memory allocated by* calling [malloc]. It is sliced into chunks, which are maintained by* the [slice] structure. It maintains additional information such as* the [size] of the memory block, the number of bytes [used] and the [next]* index at which to put a chunk.*/typedef struct _memory_block {//@ ghost booleanpacked;// ghost field [packed] is meant to be used as a guard that tells when// the invariant of a structure of type [memory_block] holdsunsigned intsize;// size of the array [data]unsigned intnext;// next index in [data] at which to put a chunkunsigned intused;// how many bytes are used in [data], not necessarily contiguous oneschar*data;// raw memory block allocated by [malloc]struct _memory_slice* slice;// structure that describes the slicing of a block into chunks} memory_block;47484950515253545556/*@ strong type invariant inv_memory_block(memory_block mb) =@ mb.packed ==>@(0 < mb.size && mb.used <= mb.next <= mb.size@&& \offset (mb.data) == 0@&& \block_length(mb.data) == mb.size) ;@@ predicate valid_memory_block(memory_block* mb) =@\valid (mb) && mb->packed ;@*/5758596061626364656667686970717273747576/* A memory chunk holds a pointer [data] to some part of a memory block* [block].

It maintains the [offset] at which it points in the block, as well* as the [size] of the block it is allowed to access. A field [free] tells* whether the chunk is used or not.*/typedef struct _memory_chunk {//@ ghost boolean packed;// ghost field [packed] is meant to be used as a guard that tells when// the invariant of a structure of type [memory_chunk] holdsunsigned intoffset;// offset at which [data] points into [block->data]unsigned intsize;// size of the chunkboolfree;// true if the chunk is not used, false otherwisememory_block* block;// block of memory into which the chunk pointschar*data;// shortcut for [block->data + offset]93APPENDIX A. APPENDICES77} memory_chunk;787980818283848586878889909192/*@ strong type invariant inv_memory_chunk(memory_chunk mc) =@ mc.packed ==>@(0 < mc.size && valid_memory_block(mc.block)@&& mc.offset + mc.size <= mc.block->next) ;@@ predicate valid_memory_chunk(memory_chunk* mc, int s) =@\valid (mc) && mc->packed && mc->size == s ;@@ predicate used_memory_chunk(memory_chunk mc) =@ mc.free == false ;@@ predicate freed_memory_chunk(memory_chunk mc) =@ mc.free == true ;@*/93949596979899100101102103104/* A memory chunk list links memory chunks in the same memory block.* Newly allocated chunks are put first, so that the offset of chunks* decreases when following the [next] pointer.

Allocated chunks should* fill the memory block up to its own [next] index.*/typedef struct _memory_chunk_list {memory_chunk*chunk;// current list elementstruct _memory_chunk_list* next;// tail of the list} memory_chunk_list;105106107108109110111112113114115116117118119120121122123124125126127128129130131132/*@ logic memory_chunk_list* next_chunk(memory_chunk_list* ptr) =@ ptr->next ;@@ predicate valid_memory_chunk_list@(memory_chunk_list* mcl, memory_block* mb) =@\valid (mcl) && valid_memory_chunk(mcl->chunk,mcl->chunk->size)@ && mcl->chunk->block == mb@ && (mcl->next == \null ||@valid_memory_chunk_list(mcl->next, mb))@ && mcl->offset == mcl->chunk->offset@ && (@// it is the last chunk in the list@(mcl->next == \null && mcl->chunk->offset == 0)@||@// it is a chunk in the middle of the list@(mcl->next != \null@&& mcl->next->chunk->offset + mcl->next->chunk->size@== mcl->chunk->offset)@)@ && finite_list(next_chunk, mcl) ;@@ predicate valid_complete_chunk_list@(memory_chunk_list* mcl, memory_block* mb) =@ valid_memory_chunk_list(mcl,mb)@ && mcl->next->chunk->offset +@mcl->next->chunk->size == mb->next ;@94A.5.

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)} */18895APPENDIX 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));96A.5.

Характеристики

Список файлов книги