ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 2
Текст из файла (страница 2)
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101A.6.7 Version 1.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101A.6.8 Version 1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101Bibliography103List of Figures105Index1077CONTENTSForewordThis is the version 1.9 of ACSL design. Several features may still evolve in the future.
Inparticular, some features in this document are considered experimental, meaning that theirsyntax and semantics is not already fixed. These features are marked with Experimental.They must also be considered as advanced features, which are not supposed to be useful fora basic use of that specification language.AcknowledgementsWe gratefully thank all the people who contributed to this document: Sylvie Boldo, JeanLouis Colaço, Pierre Crégut, David Delmas, Catherine Dubois, Stéphane Duprat, ArnaudGotlieb, Philippe Herrmann, Thierry Hubert, Dillon Pariente, Pierre Rousseau, Julien Signoles, Jean Souyris, Asma Tafat.9Chapter 1IntroductionThis document is a reference manual for the ACSL implementation provided by the Frama-Cframework [11].
ACSL is an acronym for “ANSI/ISO C Specification Language”. This is a Behavioral Interface Specification Language (BISL) implemented in the Frama-C framework.It aims at specifying behavioral properties of C source code. The main inspiration for thislanguage comes from the specification language of the Caduceus tool [9, 10] for deductiveverification of behavioral properties of C programs. The specification language of Caduceusis itself inspired from the Java Modeling Language (JML [19]) which aims at similar goals forJava source code: indeed it aims both at runtime assertion checking and static verificationusing the ESC/Java2 tool [15], where we aim at static verification and deductive verification(see Appendix A.2 for a detailed comparison between ACSL and JML).Going back further in history, JML design was guided by the general design-by-contractprinciple proposed by Bertrand Meyer, who took his own inspiration from the concepts ofpreconditions and postconditions on a routine, going back at least to Dijkstra, Floyd andHoare in the late 60’s and early 70’s, and originally implemented in the Eiffel language.In this document, we assume that the reader has a good knowledge of the ISO C programminglanguage [14, 13].1.1Organization of this documentIn this preliminary chapter we introduce some definitions and vocabulary, and discuss generalities about this specification language.
Chapter 2 presents the specification language itself.Chapter 3 presents additional information about libraries of specifications. Appendix A provides specific hindsight over type-checking ACSL annotations, the relation between ACSLand JML, and specification templates. A detailed table of contents is given on page 5. Aglossary is given in Appendix A.1.Not all of the features mentioned in this document are currently implemented in the Frama-Ckernel.
Those who aren’t yet are signaled as in the following line:This feature is not currently supported by Frama-C1As a summary, the features that are not currently implemented into Frama-C include inparticular:1Additional remarks on the feature may appear as footnote11CHAPTER 1. INTRODUCTION• some built-in predicates and logical functions;• abrupt termination clauses in statement contracts (section 2.4.4);• definition of logical types (section 2.6);• specification modules (section 2.6.11);• model variables and Model fields (section 2.59);• only basic support for ghost code is provided (section 2.12);• verification of non interference of ghost code (p.
73);• specification of volatile variables (section 2.12.1);1.2Generalities about AnnotationsIn this document, we consider that specifications are given as annotations in comments written directly in C source files, so that source files remain compilable.
Those comments muststart by /*@ or //@ and end as usual in C.In some contexts, it is not possible to modify the source code. It is strongly recommended thata tool which implements ACSL specifications provides technical means to store annotationsseparately from the source. It is not the purpose of this document to describe such means.Nevertheless, some of the specifications, namely those at a global level, can be given inseparate files: logical specifications can be imported (see Section 2.6.11) and a functioncontract can be attached to a copy of the function profile (see Section 2.3.5).1.2.1Kinds of annotations• Global annotations:– function contract : such an annotation is inserted just before the declaration orthe definition of a function. See section 2.3.– global invariant : this is allowed at the level of global declarations.
See section 2.11.– type invariant : this allows to declare both structure or union invariants, andinvariants on type names introduced by typedef . See section 2.11.– logic specifications : definitions of logic functions or predicates, lemmas, axiomatizations by declaration of new logic types, logic functions, predicates with axiomsthey satisfy.
Such an annotation is placed at the level of global declarations. Seesection 2.6• Statement annotations:– assertion : these are allowed everywhere a C label is allowed, or just before a blockclosing brace. See section 2.4.1.– loop annotation (invariant, variant, assign clauses): is allowed immediately beforea loop statement: for , while , do . . . while . See Section 2.4.2.– statement contract : very similar to a function contract, and placed before a statement or a block. Semantical conditions must be checked (no goto going inside, nogoto going outside).
See Section 2.4.4.121.3. NOTATIONS FOR GRAMMARS– ghost code : regular C code, only visible from the specifications, that is only allowedto modify ghost variables. See section 2.12. This includes ghost braces for enclosingblocks.1.2.2Parsing annotations in practiceIn JML, parsing is done by simply ignoring //@, /*@ and */ at the lexical analysis level. Thistechnique could modify the semantics of the code, for example:1return x /*@ +1 */ ;In our language, this is forbidden. Technically, the current implementation of Frama-Cisolates the comments in a first step of syntax analysis, and then parses a second time.Nevertheless, the grammar and the corresponding parser must be carefully designed to avoidinteraction of annotations with the code.
For example, in code such as12if (c) //@ assert P;c=1;the statement c=1 must be understood as the branch of the if. This is ensured by thegrammar below, saying that assert annotations are not statements themselves, but attachedto the statement that follows, like C labels.1.2.3About preprocessingThis document considers C source after preprocessing. Tools must decide how they handlepreprocessing (what to do with annotations, whether macro substitution should be performed,etc.)1.2.4About keywordsAdditional keywords of the specification language start with a backslash, if they are used inposition of a term or a predicate (which are defined in the following).
Otherwise they do notstart with a backslash (like ensures ) and they remain valid identifiers.1.3Notations for grammarsIn this document, grammar rules are given in BNF form. In grammar rules, we use extranotations e∗ to denote repetition of zero, one or more occurrences of e, e+ for repetition of oneor more occurrences of e, and e? for zero or one occurrence of e.
For the sake of simplicity, weonly describe annotations in the usual /*@ ... */ style of comments. One-line annotationsin //@ comments are alike.13Chapter 2Specification language2.1Lexical rulesLexical structure mostly follows that of ANSI/ISO C. A few differences must be noted.• The at sign (@) is a blank character, thus equivalent to a space character.• Identifiers may start with the backslash character (\).• Some UTF8 characters may be used in place of some constructs, as shown in thefollowing table:>=<=><!=====><==>&&||^^!- (unary minus)\forall\existsintegerrealboolean≥≤><6≡≡=⇒⇐⇒∧∨⊕¬−∀∃ZRB0x22650x22640x003E0x003C0x22620x22610x21D20x21D40x22270x22280x22BB0x00AC0x22120x22000x22030x21240x211D0x1D539• Comments can be put inside ACSL annotations.
They use the C++ format, i.e. beginwith // and extend to the end of current line.15CHAPTER 2. SPECIFICATION LANGUAGEliteral::=||||\true | \falseintegerrealstringcharacterboolean constantsinteger constantsreal constantsstring constantscharacter constantsbin-op::=|||+ | - | * | / | % | << | >>== | != | <= | >= | > | <&& | || | ^^& | | | --> | <--> | ^boolean operationsbitwise operationsunary-op::=||||+ |!~*&unary plus and minusboolean negationbitwise complementationpointer dereferencingaddress-of operatorterm::=|||||||||||||||||literalidunary-op termterm bin-op termterm [ term ]{ term \with [ term ] = termterm . id{ term \with .
id = term }term -> id( type-expr ) termid ( term (, term)∗ )( term )term ? term : term\let id = term ; termsizeof ( term )sizeof ( C-type-name )id : termstring : term-literal constantsvariables}array accessarray functional modifierstructure field accessfield functional modifiercastfunction applicationparenthesesternary conditionlocal bindingsyntactic namingsyntactic namingFigure 2.1: Grammar of terms2.2Logic expressionsThis first section presents the language of expressions one can use in annotations. Theseare called logic expressions in the following.
They correspond to pure C expressions, withadditional constructs that we will introduce progressively.Figures 2.1 and 2.2 present the grammar for the basic constructs of logic expressions. Inthat grammar, we distinguish between predicates and terms, following the usual distinctionbetween propositions and terms in classical first-order logic.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
