ACSL Language Reference (811287), страница 11
Текст из файла (страница 11)
SPECIFICATION LANGUAGEterm::=||||\null\base_addr one-label ? ( term )\block_length one-label ? ( term )\offset one-label ? ( term )\allocation one-label ? ( term )pred::=|||||\allocable one-label ? ( term )\freeable one-label ? ( term )\fresh two-labels ? ( term, term )\valid one-label ? ( location-address )\valid_read one-label ? ( location-address )\separated ( location-address , location-addressesone-label::={ label-idtwo-labels::={ label-id,location-addresses::=location-addresslocation-address::=tset)}label-id}(, location-address)∗Figure 2.20: Grammar extension of terms and predicates about memoryPredefined algebraic specifications can be provided as libraries (see section 3), and importedusing a construct like1//@ import List;where the file List.acsl contains logic definitions, like the List module above.2.7Pointers and physical addressingThe grammar for terms and predicates is extended with new constructs given in Figure 2.20.Location-address denotes the address of a memory location.
It is a set of terms of somepointer type as defined in Section 2.3.4.2.7.1Memory blocks and pointer dereferencingC memory is structured into allocated blocks that can come either from a declarator or acall to one of the calloc, malloc or realloc functions. Blocks are characterized by their baseaddress, i.e. the address of the declared object (the first declared object in case of an arraydeclarator), or the pointer returned by the allocating function (when the allocation succeeds)and their length.ACSL provides the following built-in functions to deal with allocated blocks. Each of themtakes an optional label identifier as argument. The default value of that label is defined inSection 2.4.3.• \base_addr{L}(p) returns the base address of the allocated block containing, at the labelL, the pointer p\base_addr{id} : void* → char*582.7.
POINTERS AND PHYSICAL ADDRESSING• \block_length{L}(p) returns the length (in bytes) of the allocated block containing, atthe label L, its argument pointer.\block_length{id} : void* → size_tIn addition, dereferencing a pointer may lead to run-time errors. A pointer p is said to bevalid if *p is guaranteed to produce a definite value according to the C standard [12]. Thefollowing built-in predicates deal with this notion:• \valid applies to a set of terms (see Section 2.3.4) of some pointer type. \valid {L}(s)holds if and only if dereferencing any p ∈ s is safe at label L, both for reading from *pand writing to it.
In particular, \valid {L}(\empty) holds for any label L.\valid {id} : set<α *> → boolean• \valid_read applies to a set of terms of some pointer type and holds if and only if it issafe to read from all the pointers in the set\valid_read {id} : set<α *> → boolean\valid {L}(s) implies \valid_read {L}(s) but the reverse is not true. In particular, it is allowedto read from a string literal, but not to write in it (see [12], 6.4.5§6).The status of \valid and \valid_read constructs depends on the type of their argument.Namely, \valid {L}((int *) p) and \valid {L}((char *)p) are not equivalent. On the otherhand, if we ignore potential alignment constraints, the following equivalence is true for anypointer p:\valid {L}(p) <==> \valid{L}(((char *)p)+(0 ..
sizeof(*p)-1))and similarly for \valid_read\valid_read {L}(p) <==> \valid_read{L}(((char *)p)+(0 .. sizeof(*p)-1))Some shortcuts are provided:• \null is an extra notation for the null pointer (i.e. a shortcut for (void*)0). As inC itself (see [12], 6.3.2.3§3), the constant 0 can have any pointer type.
In addition,\valid {L}(\null) is always false, for any logic label L. Of course, \valid_read {L}(\null)is always false too.• \offset {L}(p) returns the offset between p and its base address\offset {id}:void* → size_t\offset {L}(p) = (char*)p - \base_addr{L}(p)Again, if there are no alignment constraints, the following property holds: for any setof pointers s and label L, \valid_read {L}(s) if and only if for all p∈s:\offset {L}(p) >= 0 && \offset{L}(p) + sizeof(*p) <= \block_length{L}(p)2.7.2SeparationACSL provides a built-in function to deal with separation of locations:• \separated applies to sets of terms (see Section 2.3.4) of some pointer type.\separated (s1 ,s2 ) holds for any set of pointers s1 and s2 if and only if for all p∈s1and q∈s2 :59CHAPTER 2.
SPECIFICATION LANGUAGEallocation-clause::=|allocates dyn-allocation-addressesfrees dyn-allocation-addresses ;loop-allocation::=|looploopdyn-allocation-addresses::=|location-addresses;allocates dyn-allocation-addressesfrees dyn-allocation-addresses ;;\nothingFigure 2.21: Grammar for dynamic allocations and deallocationsforall integer i,j; 0 <= i < sizeof(*p), 0 <= j < sizeof(*q)==> (char*)p + i != (char*)q + jIn fact, \separated is an n-ary predicate.\separated (s1 ,..,sn ) means that for each i 6= j, \separated (si ,sj ).2.7.3Dynamic allocation and deallocationExperimentalAllocation-clauses allow to specify which memory location is dynamically allocated or deallocated. The grammar for those constructions is given on Figure 2.21.allocates \nothing and frees \nothing are respectively equivalent to allocates \empty andfrees \empty; it is left for convenience like for assigns clauses.Allocation clauses for function and statement contractsClauses allocates and frees are tied together.
The simple contract/*@ frees P1 ,P2 ,...;@ allocates Q1 ,Q2 ,...;@*/means that any memory address that does not belong to the union of sets of terms Pi andQj has the same allocation status (see below) in the post-state as in the pre-state. The onlydifference between allocates and frees is that sets Pi are evaluated in the pre-state, and setsQi are evaluated in the post-state.The built-in type allocation_status can take the following values:/*@type allocation_status =\static | \register | \automatic | \dynamic | \unallocated;*/Built-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))and602.7.
POINTERS AND PHYSICAL ADDRESSING\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 allocated memory block that can be safely released using the C function free. Note that\freeable { \null } does not hold, despite NULL being a valid argument to the C functionfree.\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.49 malloc and free functions can be specified as follows.12typedef unsigned long size_t;345678/*@ assigns\nothing;@ allocates \result ;@ ensures\result == \null || \fresh{Old,Here}(\result,n);@*/void *malloc(size_t n);961CHAPTER 2. SPECIFICATION LANGUAGE101112131415/*@ 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 neither of the two allocation clausesis given, 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 stating 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.50 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;@ }@*/101112131415161718192021222324/*@ allocates \result ;@ behavior allocation:@ assumes is_allocable(n);@assignsheap_status;@ensures\fresh ( \result ,n);@ behavior no_allocation:@ assumes !is_allocable(n);@assigns\nothing;@allocates \nothing;@ensures\result == \null ;@ complete behaviors ;@ disjoint behaviors ;@*/void *malloc(size_t n);25622.7.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
