ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 14
Текст из файла (страница 14)
This construct, described by the grammar of Figure 2.26, 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);75CHAPTER 2. SPECIFICATION LANGUAGEThis 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.63 The following code is instrumented in order to inject fixed values at eachread of variable x, and collect written values.volatile1int 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;161718192021222324/*@ ghost //@ requires p == &x;@ int writes_x( volatile int *p, int v) {@if (p == &x)@return collector_x[collector_count++] = v;@else@return 0; // should not happen@ }@*/2526//@ 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<α*> → bool762.13.
UNDEFINED VALUES, DANGLING POINTERSExample 2.64 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 refered to outside of itsscope, or the address of a variable that has been dynamically allocated, then deallocated.\dangling {id} : set<α*> → boolExample 2.65 In the following, the assertion holds.12345int * 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.77Chapter 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 predicate 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.79CHAPTER 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 [21]). 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 argument is really a string.Example 3.1 Here is a contract for the strcpy function:803.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.81Chapter 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 [12], or properties on evolution of data over the time, such as the historyconstraints of JML, or in the Lustre assertion language.83Appendix 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 expression is a subset of the set of C expressionswithout side effect (C standard [14, 13], §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 [16]), 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.
Not only the language features85APPENDIX A. APPENDICESare not the same but the programming styles and idioms are very different, whichentails also different ways of specifying behaviors. In particular, C has no inheritancenor exceptions, and no language support for the simplest properties on memory (e.g,the size of an allocated memory block).• JML relies on runtime assertion checking (RAC) when typing, static analysis and automatic deductive verification fail. The example of CCured [22, 7], that adds strongtyping to C by relying on RAC too, shows that it is not possible to do it in a modularway.
Indeed, it is necessary to modify the layout of C data structures for RAC, whichis not modular. The follow-up project Deputy [8] thus reduces the checking power ofannotations in order to preserve modularity. On the contrary, we choose not to restrainthe power of annotations (e.g., all first order logic formulas are allowed). To that end,we rely on manual deductive verification using an interactive theorem prover (e.g., Coq)when every other technique failed.In the remainder of this chapter, we describe these differences in further details.A.2.1Low-level language vs. inheritance-based oneNo inherited specificationsJML has a core notion of inheritance of specifications, that duplicates in specifications theinheritance feature of Java.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
