ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 17
Текст из файла (страница 17)
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 slice97APPENDIX 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;}98A.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.9• Fix typo in definition of \fresh predicate (section 2.7.3)• Fix grammar inconsistencies– use proper C rules names– fix mismatch in non-terminal names• Rename "Unspecified values" to "Dangling pointers" and precise it.
(section 2.13.2)A.6.2Version 1.8• Mention binary literal constant typing99APPENDIX A. APPENDICESA.6.3Version 1.7• Added missing shift operators in figure 2.1• Modified syntax for naming terms and predicates (figures 2.2 and 2.1)• Added syntax rule for literal constants (figure 2.1)A.6.4Version 1.6• Modified syntax for model fields (section 2.11.2)• Added missing logical xor operator (figure 2.1).• Addition of logical labels related to loops (section 2.4.3).• Addition of labels to built-ins related to memory blocks (section 2.7.1)• Introduction of \valid_read built-in and clarification of the notion of validity (section 2.7.1).• Introduction of built-in \allocable , \allocation , \freeable and \fresh (section 2.7.3).• Introduction of allocates and frees clauses (section 2.7.3).• Clarify the semantics of assigns clauses into statement contract.• Improvements to the volatile clause (section 2.12.1).• Clarify the evaluation of arrays inside an at (section 2.4.3).A.6.5Version 1.5• Clarify the status of loop invariant in presence of break or side-effects in the loop test.• Introduction of \with keyword for functional updates.• Added bnf entry for completeness of function behaviors.• Order of clauses in statement contracts is now fixed.• requires clauses are allowed before behaviors of statement contracts.• Added explicit singleton construct for sets.• Introduction of logical arrays.• Operations over pointers and arrays have been precised.• Predicate \initialized (section 2.13.1) now takes a set of pointers as argument.100A.6.
CHANGESA.6.6Version 1.4• Added UTF-8 counterparts for built-in types ( integer , real , boolean).• Fixed typos in the examples corresponding to features implemented in Frama-C.• Order of clauses in function contracts is now fixed.• Introduction of abrupt termination clauses.• Introduction of axiomatic to gather predicates, logic functions, and their defining axioms.• Added specification templates appendix for common specification issues.• Use of sets as first-class term has been precised.• Fixed semantics of predicate \separated .A.6.7Version 1.3• Functional update of structures.• Terminates clause in function behaviors.• Typos reported by David Mentré.A.6.8Version 1.2This is the first public release of this document.101BIBLIOGRAPHYBibliography[1] Jean-Raymond Abrial.
The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.[2] Ali Ayad and Claude Marché. Behavioral properties of floating-point programs. Hisseopublications, 2009. http://hisseo.saclay.inria.fr/ayad09.pdf.[3] Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In 18th IEEE International Symposium on Computer Arithmetic, pages 187–194,Montpellier, France, June 2007.[4] Patrice Chalin. Reassessing JML’s logical foundation. In Proceedings of the 7th Workshopon Formal Techniques for Java-like Programs (FTfJP’05), Glasgow, Scotland, July 2005.[5] Patrice Chalin. A sound assertion semantics for the dependable systems evolution verifying compiler.
In Proceedings of the International Conference on Software Engineering(ICSE’07), pages 23–33, Los Alamitos, CA, USA, 2007. IEEE Computer Society.[6] David R. Cok and Joseph R. Kiniry. ESC/Java2 implementation notes. Technical report,may 2007. http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/Escjava2-ImplementationNotes.pdf.[7] Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, and Westley Weimer.Ccured in the real world. In PLDI ’03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pages 232–244, 2003.[8] Jeremy Paul Condit, Matthew Thomas Harren, Zachary Ryan Anderson, David Gay, andGeorge Necula.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
