ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 13
Текст из файла (страница 13)
f.n-1];@ loop variant r - i;@*/while (i < r) {switch (t[i]) {case BLUE:swap(t, b++, i++);break;case WHITE:i++;break;case RED:swap(t, --r, i);break;}}}2.11.2Model variables and model fieldsA model variable is a variable introduced in the specification with the keyword model. Its typemust be a logic type.
Analogously, types may have model fields. These are used to provideabstract specifications to functions whose concrete implementation must remain private.The precise syntax for declaring model variables and fields is given in Figure 2.24. It ispresented as additions to the regular C grammar for declarationsInformal semantics of model variables is as follows.• Model variables can only appear in specifications. They are not lvalues, thus theydeclaration::=||C-declaration/*@ model parameter ; *//*@ model C-type-name { parameter;?} ; */model variablemodel fieldFigure 2.24: Grammar for declarations of model variables and fields702.11.
DATA INVARIANTScannot be assigned directly (unlike ghost variables, see below).• Nevertheless, a function contract might state that a model variable is assigned.• When a function contract mentions model variables:– the precondition is implicitly existentially quantified over those variables;– the postconditions are universally quantified over the old values of model variables,and existentially quantified over the new values.Thus, in practice, the only way to prove that a function body satisfies a contract with modelvariables is to provide an invariant relating model variables and concrete variables, as in theexample below.Model fields behave the same, but they are attached to any value whose static type is the oneof the model declaration.
A model field can be attached to any C type, not only to struct.When it is attached to a compound type, however, it must not have the same name as a Cfield of the corresponding type. In addition, model fields are “inherited” by a typedef in thesense that the newly defined type has also the model fields of its parents (and can acquiremore, which will not be present for the parent).
For instance, in the following code, t1 hasone model field m1, while t2 has two model fields, m1 and m2.1234typedef int t1;typedef t1 t2;/*@ model t1 { int m1 }; *//*@ model t2 { int m2 }; */Example 2.59 Here is an example of a specification for a function which generates freshintegers. The contract is given in term of a model variable which is intended to represent theset of “forbidden” values, e.g. the values that have already been generated.1/* public interface */23//@ model set<integer> forbidden = \empty;456789/*@ assigns forbidden;@ ensures ! \subset( \result ,\old(forbidden))@ && \subset( \result ,forbidden) && \subset(\old(forbidden),forbidden);@*/int gen();The contract is expressed abstractly, telling that• the forbidden set of values is modified;• the value returned is not in the set of forbidden values, thus it is “fresh”;• the new set of forbidden values contains both the value returned and the previous forbidden values.An implementation of this function might be as follows, where a decision has been made togenerate values in increasing order, so that it is sufficient to record the last value generated.This decision is made explicit by an invariant.71CHAPTER 2.
SPECIFICATION LANGUAGE12345678/* implementation */int gen() {static int x = 0;/*@ global invariant I: \forall integer k;@Set::mem(k,forbidden) ==> x > k;@*/return x++;}Remarks Although the syntax of model variables is close to JML model variables, theydiffer in the sense that the type of a model variable is a logic type, not a C type. Also, thesemantics above is closer to the one of B machines [1].
It has to be noticed that programverification with model variables does not have a well-established theoretical background [20,18], so we deliberately do not provide a precise semantics in this document .2.12Ghost variables and statementsGhost variables and statements are like C variables and statements, but visible only in thespecifications. They are introduced by the ghost keyword at the beginning of the annotation(i.e. /*@ ghost ... */ or //@ ghost ... for a one-line ghost code, as mentioned in section 1.2).The grammar is given in Figure 2.25, in which only the first form of annotation is used.In this figure, the C-* non-terminals refer to the corresponding grammar rules of the ISOstandard, without any ACSL extension. Any non terminal of the form ghost-non-term forwhich no definition is given in the figure represents the corresponding C-non-term entry, inwhich any entry is substituted by ghost-entry.The variations with respect to the C grammar are the following:• Comments must be introduced by // and extend until the end of the line (the ghostcode itself is placed inside a C comment.
/* ... */ would thus lead to incorrect Ccode).• It is however possible to write multi-line annotations for ghost code. These annotationsare enclosed between /@ and @/. As in normal annotations, @s at the beginning of a lineand at the end of the comment (before the final @/) are considered as blank.• Logical types, such as integer or real are authorized in ghost code.• A non-ghost function can take ghost parameters.
If such a ghost clause is present in thedeclarator, then the list of ghost parameters must be non-empty and fixed (no varargghost). The call to the function must then provide the appropriate number of ghostparameters.• Any non-ghost if-statement which does not have a non-ghost else clause can be augmented with a ghost one. Similarly, a non-ghost switch can have a ghost default : clauseif it does not have a non-ghost one (there are however semantical restrictions for validghost labelled statements in a switch, see next paragraph for details).722.12.
GHOST VARIABLES AND STATEMENTSghost-type-specifier::=|C-type-specifierlogic-typedeclaration::=|C-declaration/*@ ghostghost-declarationdirect-declarator::=|*/C-direct-declaratordirect-declarator( C-parameter-type-list?)/*@ ghost( ghost-parameter-type-list )*/postfix-expression::=|C-postfix-expressionpostfix-expression( C-argument-expression-list?)/*@ ghost( ghost-argument-expression-list )*/statement::=|C-statementstatements-ghoststatements-ghost::=/*@ ghostghost-statement+ghost-selection-statement::=|ghost argscall with ghosts*/C-selection-statementif ( C-expression )statement/*@ ghost elseghost-statement+*/struct-declaration::=|C-struct-declaration/*@ ghoststruct-declaration*/ghost fieldFigure 2.25: Grammar for ghost statementsSemantics of Ghost Code The question of semantics is essential for ghost code.Informally, the semantics requires that ghost statements do not change the regular programexecution3 This implies several conditions, including e.g:• Ghost code cannot modify a non-ghost C variable.• Ghost code cannot modify a non-ghost structure field.• If p is a ghost pointer pointing to a non-ghost memory location, then it is forbidden toassign *p.• Body of a ghost function is ghost code, hence do not modify non-ghost variables orfields.3Not checked in the current implementation73CHAPTER 2.
SPECIFICATION LANGUAGE• If a non-ghost C function is called in ghost code, it must not modify non-ghost variablesor fields.• If a structure has ghost fields, the sizeof of the structure is the same has the structurewithout ghost fields. Also, alignment of fields remains unchanged.• The control-flow graph of a function must not be altered by ghost statements. Inparticular, no ghost return can appear in the body of a non-ghost function. Similarly,ghost goto, break , and continue continue cannot jump outside of the innermost non-ghostenclosing block.Semantics is specified as follows. First, the execution of a program with ghost code involvesa ghost memory heap and a ghost stack, disjoint from the regular heap and stack.
Ghostvariables lie in the ghost heap, so as the ghost field of structures. Thus, every memory sideeffect can be classified as ghost or non-ghost. Then, the semantics is that memory side-effectsof ghost code must always be in the ghost heap or the ghost stack.Notice that this semantics is not statically decidable. It is left to tools to provide approximations, correct in the sense that any code statically detected as ghost must be semanticallyghost.Example 2.60 The following example shows some invalid assignments of ghost pointers:123456void f(int x, int *q) {//@ ghost int *p = q;//@ ghost *p = 0;// above assignment is wrong: it modifies *q which lies// in regular memory heap7//@ ghost p = &x;//@ ghost *p = 0;// above assignment is wrong: it modifies x which lies// in regular memory stack8910111213}Example 2.61 The following example shows some invalid ghost statements:123456789101112int f (int x, int y) {//@ ghost int z = x + y;switch (x) {case 0: return y;//@ ghost case 1: z=y;// above statement is correct.//@ ghost case 2: { z++; break; }// invalid, would bypass the non-ghost defaultdefault : y++;}return y;}13141516int g(int x) {//@ ghost int z = x;if (x > 0) { return x; }742.12.
GHOST VARIABLES AND STATEMENTS17181920}//@ ghost else { z++; return x; }// invalid, would bypass the non-ghost returnreturn x+1;Differences between model variables and ghost variables A ghost variable is anadditional specification variable which is assigned in ghost code like any C variable. On theother hand, a model variable cannot be assigned, but one can state it is modified and canexpress properties about the new value, in a non-deterministic way, using logic assertions andinvariants. In other words, specifications using ghost variable assignments are executable.Example 2.62 The example 2.59 can also be specified with a ghost variable instead of amodel variable:1//@ ghost set<integer> forbidden = \empty;2345678910111213141516/*@ assigns forbidden;@ ensures ! \subset( \result ,\old(forbidden))@ && \subset( \result ,forbidden)&& \subset(\old(forbidden),forbidden);@*/int gen() {static int x = 0;/*@ global invariant I: \forall integer k;@\subset (k,forbidden) ==> x > k;@*/x++;//@ ghost forbidden = \union(x,forbidden);return x;}2.12.1Volatile variablesExperimentalVolatile variables can not be used in logic terms, since reading such a variable may have aside effect, in particular two successive reads may return different values.declaration::=//@volatilelocations( reads id)?(writes id)?Figure 2.26: Grammar for volatile constructsSpecifying properties of a volatile variable may be done via a specific construct to attachtwo ghost functions to it.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
