ACSL Language Reference (811287), страница 15
Текст из файла (страница 15)
This construct, described by the grammar of Figure 2.28, has thefollowing shape:12volatile τ x;//@ volatile x reads f writes g;where f and g are ghost functions with the following prototypes:34τ f(volatile τ * p);τ g(volatile τ * p, τ v);This must be understood as a special construct to instrument the C code, where each accessto the variable x is replaced by a call to f(&x), and each assignment to x of a value v isreplaced by g(&x,v). If a given volatile variable is only read or only written to, the unusedaccessor function can be omitted from the volatile construct.Example 2.65 The following code is instrumented in order to inject fixed values at eachread of variable x, and collect written values.1volatileint x;23456789101112/*@ ghost //@ requires p == &x;@ int reads_x( volatile int *p) {@static int injector_x[] = { 1, 2, 3 };@static int injector_count = 0;@if (p == &x)@return injector_x[injector_count++];@else@return 0; // should not happen@ }@*/131415//@ ghost int collector_x[3];//@ ghost int collector_count = 0;1617/*@ ghost //@ requires p == &x;782.13.
UNDEFINED VALUES, DANGLING POINTERS@ int writes_x( volatile int *p, int v) {@if (p == &x)@return collector_x[collector_count++] = v;@else@return 0; // should not happen@ }@*/181920212223242526//@ volatile x reads reads_x writes writes_x;272829303132333435363738/*@ ensures collector_count == 3 && collector_x[2] == 2;@ ensures \result == 6;@*/int main () {int i, sum = 0;for (i=0 ; i < 3; i++) {sum += x;x = i;}return sum;}2.13Undefined values, dangling pointers2.13.1Initialization\initialized {L}(p) is a predicate taking a set of some pointer to l-values as argument andmeans that each l-value in this set is initialized at label L.\initialized {id} : set<α*> → boolExample 2.66 In the following, the assertion is true.12int f(int n) {int x;34567}if (n > 0) x = n ; else x = -n;//@ assert \initialized {Here}(&x);return x;Default labels are such that logic label {Here} can be omitted.2.13.2Dangling pointers\dangling {L} is a predicate taking a set of some pointer to l-values as argument and meansthat each l-value in this set has a dangling content at label L.
That, its value is (or containsbits of) a dangling address: either the address of a local variable referred to outside of itsscope, or the address of a variable that has been dynamically allocated, then deallocated.\dangling {id} : set<α*> → boolExample 2.67 In the following, the assertion holds.79CHAPTER 2. SPECIFICATION LANGUAGE12345int * f() {int a;return &a;}67891011int * g() {int * p = f();//@ assert \dangling{Here}(&p);return p+1;}In most cases, the arguments to \dangling are pointers to l-values that themselves have typepointer, so the usual signature of \dangling is actually set<α**> → bool. The signatureset<α*> → bool is useful to handle pointer values that have been written inside scalar variables through heterogeneous casts.2.14Well-typed pointersExperimentalpred::=\valid_functionlocation-address::=tset( location-address)Figure 2.29: Grammar for predicates related to well-typednessThe predicates of Figure 2.29 are used to relate the type of a pointer to the effective type ofthe memory location or function that is being pointed.Currently, only the compatibility of a function pointer with the type of the function itpoints to is axiomatized, through the predicate \valid_function .
This predicate has typeset<α*> → bool, and \valid_function (p) holds if and only if• p is a pointer to a function type t;• *p is a function whose type is compatible with t, in the sense of [12, §6.2.7]Example 2.68 In the following, the assertions are true.1int * f (int x);23456void main() {int * (*p)(int) = &f;//@ assert \valid_function ((int* (*)(int)) p); // true//@ assert \valid_function ((int* (*)()) p); // true (see C99 6.7.5.3:15)7//@ assert ! \valid_function ((void* (*)(int)) p);// not compatible: void* and int* are not compatible (see C99 6.7.5.1:2)8910111213}//@ assert ! \valid_function (( volatile int * (*)(int)) p);// not compatible: qualifiers cannot be dropped (see C99 6.7.3:9)80Chapter 3LibrariesDisclaimer: this chapter is unfinished, it is left here to give an idea of what it will look likein the final document.This chapter is devoted to libraries of specification, built upon the ACSL specification language.
Section 3.2 describes additional predicates introduced by the Jessie plugin of Frama-C,to propose a slightly higher level of annotation.3.1Libraries of logic specificationsA standard library is provided, in the spirit of the List module of Section 2.6.113.1.1Real numbersA library of general purpose functions and predicates over real numbers, floats and doubles.Includes• abs, exp, power, log, sin, cos, atan, etc. over reals• isFinite predicate over floats and doubles (means not NaN nor infinity)• rounding reals to floats or doubles with specific rounding modes.3.1.2Finite lists• pure functions nil, cons, append, fold, etc.• Path, Reachable, isFiniteList, isCyclic, etc.
on C linked-lists.3.1.3Sets and MapsFinite sets, finite maps, in ZB-style.81CHAPTER 3. LIBRARIES3.2Jessie library: logical addressing of memory blocksThe Jessie library is a collection of logic specifications whose semantics is well-defined onlyon source codes free from architecture-dependent features. In particular it is currently incompatible with pointer casts or unions (although there is ongoing work to support some ofthem [20]). As a consequence, a valid pointer of some type τ ∗ necessarily points to a memoryblock which contains values of type τ .3.2.1Abstract level of pointer validityIn the particular setting described above, it is possible to introduce the following logic functions:1234/*@@ logic integer \offset_min{L}<a>(a *p);@ logic integer \offset_max{L}<a>(a *p);@/• \offset_min {L}(p) is the minimum integer i such that (p+i) is a valid pointer at labelL.• \offset_max{L}(p) is the maximum integer i such that (p+i) is a valid pointer at labelL.The following properties hold:12\offset_min {L}(p+i) == \offset_min{L}(p)-i\offset_max{L}(p+i) == \offset_max{L}(p)-iIt also introduces some syntactic sugar:1234/*@predicate \valid_range {L}<a>(a *p,integer i,integer j) =\offset_min {L}(p) <= i && \offset_max{L}(p) >= j;*/andtheACSLbuilt-inpredicate\valid {L}(p+(a..b))isnowequivalentto\valid_range {L}(p,a,b).3.2.2StringsExperimentalThe logic function//@ logic integer \strlen (char* p);denotes the length of a 0-terminated C string.
It is a total function, whose value is nonnegativeif and only if the pointer in the argument is really a string.Example 3.1 Here is a contract for the strcpy function:823.3. MEMORY LEAKS123456789103.3/*@ // src and dest cannot overlap@ requires \base_addr(src) != \base_addr(dest);@ // src is a valid C string@ requires \strlen (src) >= 0 ;@ // dest is large enough to store a copy of src up to the 0@ requires \valid (dest+(0..\strlen(src)));@ ensures@\forall integer k; 0 <= k <= \strlen(src) ==> dest[k] == src[k];@*/char* strcpy(char *dest, const char *src);Memory leaksExperimentalVerification of absence of memory leak is outside the scope of the specification language. Onthe other hand, various models could be set up, using for example ghost variables.83Chapter 4ConclusionThis document presents a Behavioral Interface Specification Language for ANSI C sourcecode.
It provides a common basis that could be shared among several tools. The specificationlanguage described here is intended to evolve in the future and remain open to additionalconstructions. One interesting possible extension regards “temporal” properties in a largesense, such as liveness properties, which can sometimes be simulated by regular specificationswith ghost variables [11], or properties on evolution of data over the time, such as the historyconstraints of JML, or in the Lustre assertion language.85Appendix AAppendicesA.1Glossarypure expressions In ACSL setting, a pure expression is a C expression which contains noassignments, no incrementation operator ++ or --, no function call, and no access toa volatile object. The set of pure expressions is a subset of the set of C expressionswithout side effect (C standard [13, 12], §5.1.2.3, alinea 2).left-values A left-value (lvalue for short) is an expression which denotes some place in thememory during program execution, either on the stack, on the heap, or in the staticdata segment.
It can be either a variable identifier or an expression of the form *e,e[e], e.id or e->id, where e is any expression and id a field name. See C standard,§6.3.2.1 for a more detailed description of lvalues.A modifiable lvalue is an lvalue allowed in the left part of an assignment. In essence,all lvalues are modifiable except variables declared as const or of some array type withexplicit length.pre-state and post-state For a given function call, the pre-state denotes the program stateat the beginning of the call, including the current values for the function parameters.The post-state denotes the program state at the return of the call.function behavior A function behavior (behavior for short) is a set of properties relatingthe pre-state and the post-state for a possibly restricted set of pre-states (behaviorassumptions).function contract A function contract (contract for short) forms a specification of a function, consisting of the combination of a precondition (a requirement on the pre-statefor any caller to that function), a collection of behaviors, and possibly a measure incase of a recursive function.A.2Comparison with JMLAlthough we took our inspiration in the Java Modeling Language (aka JML [15]), ACSL isnotably different from JML in two crucial aspects:• ACSL is a BISL for C, a low-level structured language, while JML is a BISL for Java, anobject-oriented inheritance-based high-level language.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
