ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 10
Текст из файла (страница 10)
The logic definition123456/*@ logic integer list_length<A>(list<A> l) =@\match l {@case Nil : 0@case Cons(h,t) : 1+list_length(t)@};@*/defines the length of a list by recursion and pattern-matching.2.6.9Hybrid functions and predicatesLogic functions and predicates may take both (pure) C types and logic types arguments.Such an hybrid predicate (or function) can either be defined with the same syntax as before(or axiomatized).Be it defined either directly by an expression or through a set of axioms, an hybrid function(or predicate) usually depends on one or more program points, because it depends uponmemory states, via expressions such as:• pointer dereferencing: *p, p->f;• array access: t[i];• address-of operator: &x;• built-in predicate depending on memory: \validTo make such a definition safe, it is mandatory to add after the declared identifier a set oflabels, between curly braces, as shown on Figure 2.17.
Expressions as above must then beenclosed into the \at construct to refer to a given label. However, to ease reading of suchlogic expressions, it is allowed to omit a label whenever there is only one label in the context.Example 2.45 The following annotations declare a function which returns the number ofoccurrences of a given double in a memory block storing doubles between the given indexes,together with the related axioms. It should be noted that without labels, this axiomatizationwould be inconsistent, since the function would not depend on the values stored in t, hencethe two last axioms would say both that a==b+1 and a==b for some a and b.542.6. LOGIC SPECIFICATIONS123456789101112131415161718/*@ axiomatic NbOcc {@ // nb_occ(t,i,j,e) gives the number of occurrences of e in t[i..j]@ // (in a given memory state labelled L)@ logic integer nb_occ{L}(double *t, integer i, integer j,@double e);@ axiom nb_occ_empty{L}:@\forall double *t, e, integer i, j;@i > j ==> nb_occ(t,i,j,e) == 0;@ axiom nb_occ_true{L}:@\forall double *t, e, integer i, j;@i <= j && t[j] == e ==>@nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e) + 1;@ axiom nb_occ_false{L}:@\forall double *t, e, integer i, j;@i <= j && t[j] != e ==>@nb_occ(t,i,j,e) == nb_occ(t,i,j-1,e);@ }@*/Example 2.46 This second example defines a predicate which indicates whether two memoryblocks of the same size are a permutation of each other.
It illustrates the use of more than asingle label. Thus, the \at operator is mandatory here. Indeed the two blocks may come fromtwo distinct memory states. Typically, one of the post condition of a sorting function wouldbe permut{Pre,Post}(t,t).12345678910111213141516171819202122/*@ axiomatic Permut {@ // permut{L1,L2}(t1,t2,n) is true whenever t1[0..n-1] in state L1@ // is a permutation of t2[0..n-1] in state L2@ predicate permut{L1,L2}(double *t1, double *t2, integer n);@ axiom permut_refl{L}:@\forall double *t, integer n; permut{L,L}(t,t,n);@ axiom permut_sym{L1,L2} :@\forall double *t1, *t2, integer n;@permut{L1,L2}(t1,t2,n) ==> permut{L2,L1}(t2,t1,n) ;@ axiom permut_trans{L1,L2,L3} :@\forall double *t1, *t2, *t3, integer n;@permut{L1,L2}(t1,t2,n) && permut{L2,L3}(t2,t3,n)@==> permut{L1,L3}(t1,t3,n) ;@ axiom permut_exchange{L1,L2} :@\forall double *t1, *t2, integer i, j, n;@\at(t1[i],L1) == \at(t2[j],L2) &&@\at(t1[j],L1) == \at(t2[i],L2) &&@( \forall integer k; 0 <= k < n && k != i && k != j ==>@\at(t1[k],L1) == \at(t2[k],L2))@==> permut{L1,L2}(t1,t2,n);@ }@*/2.6.10Memory footprint specification: reads clauseExperimentalLogic declaration can be augmented with a reads clause, with the syntax given in Figure 2.18,which extends the one of Figure 2.12.
This feature allows to specify the footprint of an hybrid55CHAPTER 2. SPECIFICATION LANGUAGElogic-function-decllogic-predicate-decl::=::=logic type-expr poly-idparameters reads-clausepredicate poly-idparameters ? reads-clausereads-clause::=reads locationslogic-function-def::=logic type-expr poly-idparameters reads-clauselogic-predicate-def::=predicate poly-idparameters ? reads-clause;;= term= pred;;Figure 2.18: Grammar for logic declarations with reads clausespredicate or function, that is the set of memory locations which it depends on.
From suchan information, one might deduce properties of the form f {L1 }(args) = f {L2 }(args) if it isknown that between states L1 and L2 , the memory changes are disjoint from the declaredfootprint.Example 2.47 The following is the same as example 2.45 augmented with a reads clause.12345678910/*@ axiomatic Nb_occ {@ logic integer nb_occ{L}(double *t, integer i, integer j,@double e)@reads t[i..j];@@ axiom nb_occ_empty{L}: // ...@@ // ...@ }@*/If for example a piece of code between labels L_1 and L_2 modifies t[k] for some index koutside i..j, then one can deduce that nb_occ{L_1}(t,i,j,e)==nb_occ{L_2}(t,i,j,e).2.6.11Specification ModulesSpecification modules can be provided to encapsulate several logic definitions, for example1234567891011121314/*@ module List {@@ type list<A> = Nil | Cons(A , list<A>);@@logic integer length<A>(list<A> l) =@\match l {@case Nil : 0@case Cons(h,t) : 1+length(t) } ;@@logic A fold_right<A,B>((A -> B -> B) f, list<A> l, B acc) =@\match l {@case Nil : acc@case Cons(h,t) : f(h,fold_right(f,t,acc)) } ;562.7.
POINTERS AND PHYSICAL ADRESSINGterm::=||||\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::={ idtwo-labels::={ id,location-addresses::=location-addresslocation-address::=tset)}id}(, location-address)∗Figure 2.19: Grammar extension of terms and predicates about memory@@logic list<A> filter<A>((A -> boolean) f, list<A> l) =@fold_right((\lambda A x, list<A> acc;@f(x) ? Cons(x,acc) : acc), Nil) ;@@ }@*/15161718192021Module components are then accessible using a qualified notation like List::length.Predefined algebraic specifications can be provided as libraries (see section 3), and importedusing a construct like1//@ open List;where the file list.acsl contains logic definitions, like the List module above.2.7Pointers and physical adressingGrammar for terms and predicates is extended with new constructs given in Figure 2.19.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 succeed)and their length.57CHAPTER 2. SPECIFICATION LANGUAGEACSL provides the following built-in functions to deal with allocated blocks.
All 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*• \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 [13]. 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 [13], 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)))and\valid_read {L}(p) <==> \valid_read{L}(((char *)p)+(0..sizeof(*p)))Some shortcuts are provided:• \null is an extra notation for the null pointer (i.e.
a shortcut for (void*)0). As inC itself (see [13], 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 is no alignment constraints, the following property holds: for any set ofpointers 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)582.7. POINTERS AND PHYSICAL ADRESSINGallocation-clause::=|allocates dyn-allocation-addressesfrees dyn-allocation-addresses ;loop-allocation::=|looploopdyn-allocation-addresses::=|location-addresses;allocates dyn-allocation-addressesfrees dyn-allocation-addresses ;;\nothingFigure 2.20: Grammar for dynamic allocations and deallocations2.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 :forall 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.20.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 and Qjhas the same allocation status (see below) in the post-state than in the pre-state. The onlyone difference between allocates and frees is that sets Pi are evaluated in the pre-state, andsets Qi 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;*/59CHAPTER 2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
