ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 11
Текст из файла (страница 11)
SPECIFICATION LANGUAGEBuilt-in function \allocation {L}(p) returns the allocation status of the block containing, atthe label L, the pointer p\allocation {id} : void* → allocation_statusThis function is such that for any pointer p and label L\allocation {L}(p) == \allocation{L}(\base_addr(p))and\allocation {L}(p)==\unallocated ==> !\valid_read{L}(p)allocates Q1 ,. . .,Qn is equivalent to the postcondition\forall char* p;\separated (\union(Q1 ,.
. .,Qn ),p)==>(\base_addr{Here}(p)==\base_addr{Pre}(p)&& \block_length{Here}(p)==\block_length{Pre}(p)&& \valid {Here}(p)<==>\valid{Pre}(p)&& \valid_read{Here}(p)<==>\valid_read{Pre}(p)&& \allocation {Here}(p)==\allocation{Pre}(p))In fact, like the assigns clause does not specify which memory location is assigned, theallocation-clauses do not specify which memory location is dynamically allocated or deallocated. Pre-conditions and post-conditions should be added to complete specifications aboutallocations and deallocations.
The following shortcuts can be used for that:• \allocable {L}(p) holds if and only if the pointer p refers, at the label L, to the baseaddress of an unallocated memory block.\allocable {id} : void* → booleanFor any pointer p and label L\allocable {L}(p) <==> (\allocation{L}(p)==\unallocated && p==\base_addr{L}(p)).• \freeable {L}(p) holds if and only if the pointer p refers, at the label L, to an allocatedmemory block that can be safely released using the C function free.\freeable {id} : void* → booleanFor any pointer p and label L\freeable {L}(p) <==> (\allocation{L}(p)==\dynamic && p==\base_addr{L}(p)).• \fresh {L0 ,L1 }(p,n) , indicates that p refers to an allocated memory block at label L1 ,but that it is not the case at label L0 .
The predicate ensures also that, at label L1 , thelength (in bytes) of the block allocated dynamically equals to n.\fresh {id,id} : void*, integer → booleanFor any pointer p and labels L0 and L1\fresh {L0 ,L1 }(p,n) <==> (\allocable{L0 }(p) &&\freeable {L1 }(p) &&\block_length{L1 }(p)==n &&\valid {L1 }((char*)p+(0 .. (n-1)))Example 2.48 malloc and free functions can be specified as follows.602.7. POINTERS AND PHYSICAL ADRESSING12typedef unsigned long size_t;345678/*@ assigns\nothing;@ allocates \result ;@ ensures\result == \null || \fresh{Old,Here}(\result,n);@*/void *malloc(size_t n);9101112131415/*@ requires p!=\null ==> \freeable {Here}(p);@ assigns \nothing;@ freesp;@ ensures p!=\null ==> \allocable {Here}(p);@*/void free(void *p);Default labels for constructs dedicated to memory are such that logic label Here can be omitted.When a behavior contains only one of the two allocation clauses, the given clause specifiesthe whole set of memory addresses to consider.
This means that the set value for the otherclause of that behavior defaults to \nothing . Now, when none of the two allocation clauses isgiven, the meaning is different for anonymous behaviors and named behaviors:• a named behavior without allocation clause does not specify anything about allocationsand deallocations. The allocated and deallocated memory blocks are in fact specifiedby the anonymous behavior of the contract. There is no condition to verify for thesenamed behaviors about allocations and deallocations;• for an anonymous behavior, no allocation clause means that there is no newly allocatednor deallocated memory block. That is equivalent to give allocates \nothing .These rules are such that contracts without any allocation clause should be considered ashaving only one allocates \nothing; leading to a condition to verify for each anonymousbehavior.Example 2.49 More precise specifications can be given using named behaviors under theassumption of assumes clauses.12typedef unsigned long size_t;3456789//@ ghost int heap_status;/*@ axiomatic dynamic_allocation {@predicate is_allocable(size_t n) // Can a block of n bytes be allocated?@reads heap_status;@ }@*/10111213141516/*@ allocates \result ;@ behavior allocation:@ assumes is_allocable(n);@assignsheap_status;@ensures\fresh ( \result ,n);@ behavior no_allocation:61CHAPTER 2.
SPECIFICATION LANGUAGE1718192021222324@ assumes !is_allocable(n);@assigns\nothing;@allocates \nothing;@ensures\result == \null ;@ complete behaviors ;@ disjoint behaviors ;@*/void *malloc(size_t n);252627282930313233343536373839/*@ frees p;@ behavior deallocation:@ assumes p!=\null;@requires \freeable (p);@assigns heap_status;@ensures \allocable (p);@ behavior no_deallocation:@ assumes p==\null;@assigns \nothing;@frees\nothing;@ complete behaviors ;@ disjoint behaviors ;@*/void free(void *p);The behaviors named allocation and deallocation do not need an allocation clause. Forexample, the allocation constraint of the allocation behavior is given by the clause allocates\result of the anonymous behavior of the malloc function contract.
To set a stronger contraintinto the behavior named no_allocation, the clause allocates \nothing should be given.Allocation clauses for loop annotationsLoop annotations are complemented by similar clauses allowing to specify which memory location is dynamically allocated or deallocated by a loop. The grammar for those constructionsis given on Figure 2.20.The clauses loop allocates and loop frees are tied together.
The simple loop annotation/*@ loop frees P1 ,P2 ,...;@ loop allocates Q1 ,Q2 ,...; */means that any memory address that does not belong to the union of sets of terms Pi and Qihas the same allocation status in the current state than before entering the loop. The onlydifference between these two clauses is that sets Pi are evaluated in the state before enteringthe loop (label LoopEntry), and Qi are evaluated in the current loop state (label LoopCurrent).Namely, as for loop assigns , loop annotations loop frees and loop allocates define a loopinvariant.More precisely, the following loop annotation://@ loop allocates Q1 ,...,Qn ; */is equivalent to the loop invariant:\forall char* p;\separated (\union(Q1 ,. . .,Qn ),p) ==>(\base_addr{Here}(p)==\base_addr{LoopEntry}(p)&& \block_length{Here}(p)==\block_length{LoopEntry}(p)622.8.
SETS AS FIRST-CLASS VALUES&& \valid {Here}(p)<==>\valid{LoopEntry}(p)&& \valid_read{Here}(p)<==>\valid_read{LoopEntry}(p)&& \allocation {Here}(p)==\allocation{LoopEntry}(p))Example 2.501234567891011/*@/*@@@assert \forall integer j; 0<=j<n ==> \freeable(q[j]); */loop assignsq[0..(i-1)];loop freesq[0..\at(i-1,LoopCurrent)];loop invariant \forall integer j ;0 <= j < i ==> \allocable(\at(q[j],LoopEntry));@ loop invariant \forall integer j ; 0 <= i <= n;@*/for (i=0; i<n; i++) {free(q[i]);q[i]=NULL;}12The addresses of locations q[0..n] are not modified by the loop, but their values are.
Theclause loop frees catches the set of the memory blocks that may have been released by theprevious loop iterations. The first loop invariant defines exactly these memory blocks. Onthe other hand, loop frees indicates that the remaining blocks have not been freed since thebeginning of the loop. Hence, they are still \freeable as expressed by the initial assert , andfree(q[i]) will succeed at next step.A loop-clause without allocation clause implicitly contents loop allocates \nothing . Thatmeans the allocation status is not modified by the loop body.
A loop-behavior withoutallocation clause means that the allocated and deallocated memory blocks are in fact specifiedby the allocation clauses of the loop-clauses (Grammar of loop-clauses and loop-behaviors isgiven in Figure 2.9).2.8Sets as first-class valuesSets of terms, as defined in Section 2.3.4, can be used as first-class values in annotations. Allthe elements of such a set must share the same type (modulo the usual implicit conversions).Sets have the built-in type set<A> where A is the type of terms contained in the set.In addition, it is possible to consider sets of pointers to values of different types.
Inthis case, the set is of type set<char*> and each of its elements e is converted to(char*)e + (0..sizeof(*e)-1).Example 2.51 The following example defines the footprint of a structure, that is the set oflocations that can be accessed from an object of this type.1234struct S {char *x;int *y;};56//@ logic set<char*> footprint(struct S s) = \union(s.x,s.y) ;763CHAPTER 2. SPECIFICATION LANGUAGEabrupt-clause-fn::=exits-clauseexits-clause::=exits predabrupt-clause-stmt::=|exits-clausebreaks-clausebreaks-clause::=breaks predcontinues-clause::=continues predreturns-clause::=returns predterm::=\exit_status;| continues-clause| returns-clause;;;Figure 2.21: Grammar of contracts about abrupt terminations8910/*@ logic set<char*> footprint2(struct S s) =@\union(s.x,(char*)s.y+(0..sizeof(s.y)-1)) ;@*/111213141516/*@ axiomatic Conv {axiom conversion: \forall struct S s;footprint(s) == \union(s.x,(char*) s.y + (0 ..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
