Authors Julien Signoles
License CC-BY-SA-4.0
E-ACSL
Executable ANSI/ISO C Specification Language
Version 1.19 – Implementation in Frama-C E-ACSL version 27.1
Julien Signoles
Work licensed under Creative Commons BY-SA licence
https://creativecommons.org/licenses/by-sa/4.0/
© 2011-2023 CEA LIST
Contents
1 Introduction 5
1.1 Organization of this document . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2 Generalities about Annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Notations for grammars . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2 Specification language 7
2.1 Lexical rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Logic expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2.1 Operators precedence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.3 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2.4 Integer arithmetic and machine integers . . . . . . . . . . . . . . . . . 13
2.2.5 Real numbers and floating point numbers . . . . . . . . . . . . . . . . 13
2.2.6 C arrays and pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2.7 Structures, Unions and Arrays in logic . . . . . . . . . . . . . . . . . . 13
2.3 Function contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3.1 Built-in constructs \old and \result . . . . . . . . . . . . . . . . . . 13
2.3.2 Simple function contracts . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.3 Contracts with named behaviors . . . . . . . . . . . . . . . . . . . . . . 15
2.3.4 Memory locations and sets of terms . . . . . . . . . . . . . . . . . . . . 15
2.3.5 Default contracts, multiple contracts . . . . . . . . . . . . . . . . . . . 15
2.4 Statement annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.4.1 Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.4.2 Loop annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.4.3 Built-in construct \at . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.4.4 Statement contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5 Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5.1 Integer measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5.2 General measures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5.3 Recursive function calls . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5.4 Non-terminating functions . . . . . . . . . . . . . . . . . . . . . . . . . 20
2
CONTENTS
2.6 Logic specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.6.1 Predicate and function definitions . . . . . . . . . . . . . . . . . . . . . 22
2.6.2 Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.6.3 Inductive predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.6.4 Axiomatic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.6.5 Polymorphic logic types . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.6.6 Recursive logic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.6.7 Higher-order logic constructions . . . . . . . . . . . . . . . . . . . . . . 22
2.6.8 Concrete logic types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.6.9 Hybrid functions and predicates . . . . . . . . . . . . . . . . . . . . . . 25
2.6.10 Memory footprint specification: reads clause . . . . . . . . . . . . . . 25
2.6.11 Specification Modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.7 Pointers and physical adressing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.7.1 Memory blocks and pointer dereferencing . . . . . . . . . . . . . . . . . 25
2.7.2 Separation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.7.3 Dynamic allocation and deallocation . . . . . . . . . . . . . . . . . . . 26
2.8 Sets and lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.8.1 Finite sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.8.2 Finite lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.9 Abrupt termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.10 Dependencies information . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.11 Data invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.11.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.11.2 Model variables and model fields . . . . . . . . . . . . . . . . . . . . . 28
2.12 Ghost variables and statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.12.1 Volatile variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.13 Initialization and undefined values . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.14 Dangling pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.15 Well-typed pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.16 Logic attribute annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.17 Preprocessing for ACSL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3 Libraries 31
4 Conclusion 32
A Appendices 33
A.1 Changes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
A.2 Changes in E-ACSL Implementation . . . . . . . . . . . . . . . . . . . . . . . . . 35
Bibliography 37
List of Figures 38
Index 39
3
Foreword
This document describes version 1.19 of the E-ACSL specification language. It is based on the ACSL
specification language [2]. Features of both languages may still evolve in the future, even if we do our best
to preserve backward compatibility. In particular, some features are considered experimental, meaning
that their syntax and semantics is not yet fixed. These features are marked with Experimental.
Acknowledgements
We gratefully thank all the people who contributed to this document: Patrick Baudin, Bernard Botella,
Thibaut Benjamin, Loïc Correnson, Pascal Cuoq, Basile Desloges, Johannes Kanig, André Maroneze,
Fonenantsoa Maurica, David Mentré, Benjamin Monate, Yannick Moy and Virgile Prevosto.
This work has been initially supported by the ‘Hi-Lite’ FUI project (FUI AAP 9).
4
Introduction 1
This document is a reference manual for the E-ACSL implementation provided by the E-ACSL plug-
in [11] (version27.1) of the Frama-C framework [7]. E-ACSL is an acronym for “Executable ANSI/ISO
C Specification Language”. It is an “executable” subset of ACSL [2] implemented [3] in the Frama-C
platform [7]. Contrary to ACSL, each E-ACSL specification is executable: it may be evaluated at
runtime.
In this document, we assume that the reader has a good knowledge of both ACSL [2] and the ANSI
C programming language [8, 9].
1.1 Organization of this document
This document is organized in the very same way that the reference manual of ACSL [2].
Instead of being a fully new reference manual, this document points out the differences between
E-ACSL and ACSL. Each E-ACSL construct which is not pointed out must be considered to have the
very same semantics than its ACSL counterpart. For clarity, each relevant grammar rules are given
in BNF form in separate figures like the ACSL reference manual does. In these rules, constructs with
semantic changes are displayed in blue.
Not all of the features mentioned in this document are currently implemented in the Frama-C’s
E-ACSL plug-in. Those who aren’t yet are signaled as in the following line:
This feature is not currently supported by Frama-C’s E-ACSL plug-in.1
As a summary, Figure 1.1 synthetizes main features that are not currently implemented into the
Frama-C’s E-ACSL plug-in.
1.2 Generalities about Annotations
No difference with ACSL.
1.3 Notations for grammars
No difference with ACSL.
1 Additional remarks on the feature may appear as footnote.
5
1.3. NOTATIONS FOR GRAMMARS
typing mathematical reals
terms truth values \true and \false
functional updates
irrational numbers
built-in function \length over arrays
conversions of structure to structure
t-sets
abstractions
\max and \min
hybrid functions
labeled memory-related built-in functions
finite sets
finite lists
\exit_status
predicates let bindings of predicates
unguarded quantifications over small types
quantifications over pointers and enums
iterators
comparisons of unions and structures
t-sets
hybrid predicates
labeled memory-related built-in predicates
dangling pointers \dangling
clauses decreases clauses
assigns clauses
allocation and deallocation clauses
abrupt clauses
reads clauses
annotations behavior-specific annotations (introduced by for)
loop assigns
loop allocations
lemmas
inductive predicates
axiomatic definitions
polymorphic logic types
concrete logic types
specification modules
data invariants
model variables and model fields
volatile variables
Figure 1.1: Summary of not-yet-implemented features.
6
Specification language 2
2.1 Lexical rules
No difference with ACSL.
2.2 Logic expressions
No difference with ACSL, but the quantifications must be guarded.
More precisely, the grammars of terms and binders presented respectively Figures 2.1 and 2.3 are the
same than the ones of ACSL, while Figure 2.2 presents the grammar of predicates. The only differences
introduced by E-ACSL with respect to ACSL are the fact that the quantifications that must be guarded
and the introduction of iterators.
Quantification
The general form of quantifications (called generalized quantifications below), as described in Fig. 2.2, is
restricted to a few finite enumerable types: the types of bound variables must be C integer types, enum
types, pointer types, or their aliases.
Generalized quantification over large types (for instance, types containing 232 elements). are unlikely
evaluated efficiently at runtime.
In addition to generalized quantifications, a restricted form of guarded quantifications described in
Fig. 2.4 is also recognized for (possibly infinite) enumerable types (typically, integer). In guarded
quantifications, each bound variable must be guarded exactly once and, if its bounds depend on other
bound variables, these variables must be guarded earlier or guarded by the same guard. Additionnally,
guards are limited to bound variables, meaning that the only allowed identifiers id are variable identifiers
enclosed in the binder list.
Guarded quantifications over pointer types and enum types are not yet implemented.
Example 2.1 The following predicates are (labeled) guarded quantifications:
– sorted: \forall integer i, j; 0 <= i <= j < len ==> a[i] <= a[j]
– is_c: \exists u8 *q; p <= q < p + len && *q == (u8)c
Iterator quantification
For iterating over other data structures, E-ACSL introduces a notion of iterators over types that are
introduced by a specific construct which attaches two sets — namely nexts and guards — to a binary
predicate over a type τ . This construct is described by the grammar of Figure 2.5. For a type τ , nexts
is a set of terms, and guards a set of predicates of the same cardinal. Each term in nexts is a function
7
2.2. LOGIC EXPRESSIONS
literal ::= \true | \false boolean constants
| integer (lexical) integer constants
| real (lexical) real constants
| string (lexical) string constants
| character (lexical) character constants
bin-op ::= + | - | * | / | %
| == | != | <= | >= | > | <
| && | || | ^^ boolean operations
| << | >>
| & | | | --> | <--> | ^ bitwise operations
unary-op ::= + | - unary plus and minus
| ! boolean negation
| ~ bitwise complementation
| * pointer dereferencing
| & address-of operator
term ::= literal literal constants
| id variables, function names
| unary-op term
| term bin-op term
| term [ term ] array access
| { term
\with [ term ] = term } array functional modifier
| term . id structure field access
| { term \with . id = term } field functional modifier
| term -> id
| ( type-expr ) term cast
| id ( term (, term)∗ ) function application
| ( term ) parentheses
| term ? term : term ternary condition
| \let id = term ; term local binding
| sizeof ( term )
| sizeof ( C-type-expr )
| id : term syntactic naming
| string : term syntactic naming
poly-id ::= id
ident ::= id
Figure 2.1: Grammar of terms. The terminals id, C-type-name, and various literals are the same as the
corresponding C lexical tokens.
8
2.2. LOGIC EXPRESSIONS
rel-op ::= == | != | <= | >= | > | <
pred ::= \true | \false
| term (rel-op term)+ comparisons
| id ( term (, term)∗ ) predicate application
| ( pred ) parentheses
| pred && pred conjunction
| pred || pred disjunction
| pred ==> pred implication
| pred <==> pred equivalence
| ! pred negation
| pred ^^ pred exclusive or
| term ? pred : pred ternary condition
| pred ? pred : pred
| \let id = term ; pred local binding
| \let id = pred ; pred
| \forall binders ;
integer-guards ==> pred univ. integer quantification
| \exists binders ;
integer-guards && pred exist. integer quantification
| \forall binders ;
iterator-guard ==> pred univ. iterator quantification
| \exists binders ;
iterator-guard && pred exist. iterator quantification
| \forall binders ; pred univ. quantification
| \exists binders ; pred exist. quantification
| id : pred syntactic naming
| string : pred syntactic naming
integer-guards ::= interv (&& interv)∗
interv ::= (term integer-guard-op)+
id
(integer-guard-op term)+
integer-guard-op ::= <= | <
iterator-guard ::= id ( term , term )
Figure 2.2: Grammar of predicates
9
2.2. LOGIC EXPRESSIONS
binders ::= binder (, binder)∗
binder ::= type-expr variable-ident
(,variable-ident)∗
type-expr ::= logic-type-expr | C-type-name
logic-type-expr ::= built-in-logic-type
| id type identifier
built-in-logic-type ::= boolean | integer | real
variable-ident ::= id | * variable-ident
| variable-ident []
| ( variable-ident )
Figure 2.3: Grammar of binders and type expressions
guarded-quantif ::= \forall binders ; (guards ==>)+ pred
| \exists binders ; guards && pred
guards ::= interv (&& interv)∗
interv ::= term (guard-op id)+ guard-op term
guard-op ::= <= | <
Figure 2.4: Grammar of guarded quantifications.
iterator ::= \forall binders ; iterator-guard ==> pred
| \exists binders ; iterator-guard && pred
iterator-guard ::= id ( term , term )
declaration ::= //@ iterator id ( wildcard-param , wildcard-param ) :
nexts terms ; guards predicates ;
wildcard-param ::= parameter
| _
terms ::= term (, term)∗
predicates ::= predicate (, predicate)∗
Figure 2.5: Grammar of iterator declarations
10
2.2. LOGIC EXPRESSIONS
taking an argument of type τ and returning a value of type τ which is a successor of its argument. Each
predicate in the set guards takes an element of type τ , and is valid (resp. invalid) to indicate that the
iteration should continue on the corresponding successor (resp. stop at the given argument).
Furthermore, the guard of a quantification using an iterator must be the predicate given in the
definition of the iterator. This abstract binary predicate takes two arguments of the same type. One of
them must be unnamed by using a wildcard (character underscore ’_’). The unnamed argument must
be bound to the quantifier, while the other corresponds to the term from which the iteration begins.
Example 2.2 The following example introduces binary trees and a predicate which is valid if and only
if each value of a binary tree is even.
struct btree {
int val;
struct btree *left, *right;
};
/*@ iterator access(_, struct btree *t):
@ nexts t->left, t->right;
@ guards \valid(t->left), \valid(t->right); */
/*@ predicate is_even(struct btree *t) =
@ \forall struct btree *tt; access(tt, t) ==> tt->val % 2 == 0; */
2.2.1 Operators precedence
No difference with ACSL.
Figure 2.6 summarizes operator precedences.
class associativity operators
selection left [· · ·]-> .
unary right ! ~ + - * & (cast) sizeof
multiplicative left */%
additive left +-
shift left << >>
comparison left < <= > >=
comparison left == !=
bitwise and left &
bitwise xor left ^
bitwise or left |
bitwise implies left -->
bitwise equiv left <-->
connective and left &&
connective xor left ^^
connective or left ||
connective implies right ==>
connective equiv left <==>
ternary connective right · · ·?· · ·:· · ·
binding left \forall \exists \let
naming right :
Figure 2.6: Operator precedence
11
2.2. LOGIC EXPRESSIONS
2.2.2 Semantics
No difference with ACSL, but undefinedness and same laziness than C.
More precisely, while ACSL is a 2-valued logic with only total functions, E-ACSL is a 3-valued logic
with partial functions since terms and predicates may be “undefined”.
In this logic, the semantics of a term denoting a C expression e is undefined if e leads to a runtime
error. Consequently the semantics of any term t (resp. predicate p) containing a C expression e leading
to a runtime error is undefined if e has to be evaluated in order to evaluate t (resp. p).
Example 2.3 The semantics of all the below predicates are undefined:
– 1/0 == 1/0
– f(*p) for any logic function f and invalid pointer p
Furthermore, C-like operators &&, ||, and _ ? _ : _ are lazy like in C: their right members
are evaluated only if required. Thus the amount of undefinedness is limited. Consequently, predicate
p ==> q is also lazy since it is equivalent to !p || q. It is also the case for guarded quantifications since
guards are conjunctions and for ternary condition since it is equivalent to a disjunction of implications.
Example 2.4 All the predicates below are well defined. The first, second and fourth predicates are
invalid, whereas the third one is valid:
– \false && 1/0 == 1/0
– \forall integer x, -1 <= x <= 1 ==> 1/x > 0
– \forall integer x, 0 <= x <= 0 ==> \false ==> -1 <= 1/x <= 1
– \exists integer x, 1 <= x <= 0 && -1 <= 1/0 <= 1
In particular, the second one is invalid since the quantification is in fact an enumeration over a
finite number of elements, it amounts to 1/-1 > 0 && 1/0 > 0 && 1/1 > 0. The first atomic
proposition is invalid, so the rest of the conjunction (and in particular 1/0) is not evaluated. The fourth
one is invalid since it is an existential quantification over an empty range.
A contrario the semantics of the predicates below is undefined:
– 1/0 == 1/0 && \false
– -1 <= 1/0 <= 1 ==> \true
– \exists integer x, -1 <= x <= 1 && 1/x > 0
Furthermore, casting a term denoting a C expression e to a smaller type τ is undefined if e is not
representable in τ .
Example 2.5 Below, the first term is well-defined, while the second one is undefined.
– (char)127
– (char)128
Handling undefinedness in tools It is the responsibility of each tool which interprets E-ACSL to
ensure that an undefined term is never evaluated. For instance, it may exit with a proper error message
or, if it generates C code, it may guard each generated undefined C expression in order to be sure that
they are always safely used.
The E-ACSL plug-in of Frama-C generates such guards. Yet, a few guards are still missing.
This behavior is consistent with both ACSL [2] and mainstream specification languages for runtime
assertion checking like JML [10]. Consistency means that, if it exists and is defined, the E-ACSL
predicate corresponding to a valid (resp. invalid) ACSL predicate is valid (resp. invalid). Thus it is
possible to reuse tools interpreting ACSL (e.g., Frama-C’s Eva [4] or Wp [1] in order to interpret
E-ACSL, and it is also possible to perform runtime assertion checking of E-ACSL predicates in the
same way than JML predicates. Reader interested by the implications (especially issues) of such a
choice may read the articles of Patrice Chalin on that topic [5, 6].
12
2.3. FUNCTION CONTRACTS
2.2.3 Typing
No difference with ACSL.
2.2.4 Integer arithmetic and machine integers
No difference with ACSL.
2.2.5 Real numbers and floating point numbers
No difference with ACSL, but no quantification over real numbers and floating point numbers.
Exact real numbers and even operations over floating point numbers are usually difficult to implement.
Thus, most tools may not support them (or may support them partially).
More precisely, most real numbers are not representable at runtime with an infinite precisions.
Consequently, most operations over them (e.g., equality) cannot be computed at runtime with an
arbitrary precision. In such cases, it is the responsibility of each tool which interprets E-ACSL to
specify the level of precision (e.g., 1e−6 ) up to which it is sound, and/or to emit undefinitive verdicts
(e.g., “unknown”).
Only floating point numbers (e.g., 0.1f), rationals numbers (in Q) and operations over them are
supported by the E-ACSL plug-in. Real numbers that are irrational numbers are not supported.
2.2.6 C arrays and pointers
No difference with ACSL.
Ensuring validity of memory accesses is usually difficult to implement, since it requires the imple-
mentation of a memory model. Thus, most tools may not support it (or may support it partially).
2.2.7 Structures, Unions and Arrays in logic
No difference with ACSL.
Logic arrays without an explicit length are usually difficult to implement. Thus, most tools may not
support them (or may support them partially).
The following constructs are currently not supported by the E-ACSL plug-in:
– built-in function \length;
– comparisons of unions and structures;
– functional updates;
– conversions of structure to structure.
2.3 Function contracts
No difference with ACSL, but no clause terminates.
Figure 2.7 shows the grammar of function contracts. This is a simplified version of ACSL one
without terminates clauses. Section 2.5 explains why E-ACSL has no terminates clause.
2.3.1 Built-in constructs \old and \result
No difference with ACSL.
Figure 2.8 summarizes the grammar extension of terms with \old and \result.
13
2.3. FUNCTION CONTRACTS
function-contract ::= requires-clause ∗
decreases-clause ? simple-clause ∗
named-behavior ∗ completeness-clause ∗
clause-kind ::= check | admit
requires-clause ::= clause-kind ? requires pred ;
decreases-clause ::= decreases term (for ident)? ;
simple-clause ::= assigns-clause | ensures-clause
| allocation-clause | abrupt-clause
assigns-clause ::= assigns locations ;
locations ::= locations-list | \nothing
∗
locations-list ::= location (, location)
location ::= tset
ensures-clause ::= clause-kind ? ensures pred ;
named-behavior ::= behavior id : behavior-body
∗
behavior-body ::= assumes-clause requires-clause ∗ simple-clause ∗
assumes-clause ::= assumes pred ;
completeness-clause ::= complete behaviors (id (, id)∗ )? ;
| disjoint behaviors (id (, id)∗ )? ;
Figure 2.7: Grammar of function contracts
term ::= \old ( term ) old value
| \result result of a function
pred ::= \old ( pred )
Figure 2.8: \old and \result in terms
14
2.3. FUNCTION CONTRACTS
2.3.2 Simple function contracts
No difference with ACSL.
assigns is usually difficult to implement, since it requires the implementation of a memory model.
Thus, most tools may not support it (or may support it partially).
2.3.3 Contracts with named behaviors
No difference with ACSL.
2.3.4 Memory locations and sets of terms
No difference with ACSL, but ranges and set comprehensions are limited in order to be finite.
Figure 2.9 describes the grammar of sets of terms. There are two differences with ACSL:
– ranges necessarily have lower and upper bounds;
– a guard for each binder is required when defining set comprehension. The requested constraints
for guards are the very same than the ones for quantifications.
range ::= term .. term
tset ::= \empty empty set
| tset -> id
| tset . id
| * tset
| & tset
| tset [ tset ]
| tset [ range ]
| ( range ) a range as a set of integers
| \union ( tset (, tset)∗ ) union of location sets
| \inter ( tset (, tset)∗ ) intersection of location sets
| tset + tset
| ( tset )
| { tset | binders ; constraints } set comprehension
| { (term (, term)∗ )? } explicit set
| term implicit singleton
pred ::= \subset ( tset , tset ) set inclusion
| term \in tset set membership
constraints ::= guards (&& pred)?
Figure 2.9: Grammar for sets of terms
Example 2.6 The set { x | integer x; 0 <= x <= 10 && x % 2 == 0} denotes the set of
even integers between 0 and 10.
Ranges are currently only supported in memory built-ins described in Section 2.7.1, 2.13 and 2.14.
Example 2.7 The predicate \valid(&t[0 .. 9]) is supported and denotes that the ten first cells
of the array t are valid. Writing the term &t[0 .. 9] alone, outside any memory built-in, is not yet
supported.
2.3.5 Default contracts, multiple contracts
No difference with ACSL.
15
2.4. STATEMENT ANNOTATIONS
2.4 Statement annotations
2.4.1 Assertions
No difference with ACSL.
Figure 2.10 summarizes the grammar for assertions.
C-compound-statement ::= { C-declaration∗
C-statement∗ assertion+ }
C-statement ::= assertion
C-statement
assertion-kind ::= assert assertion
| clause-kind non-blocking assertion
assertion ::= /*@ assertion-kind pred ;
*/
| /*@ for id (, id)∗ :
assertion-kind pred ;
*/
Figure 2.10: Grammar for assertions
2.4.2 Loop annotations
No difference with ACSL, but loop invariants lose their inductive nature.
Figure 2.11 shows the grammar for loop annotations. There is no syntactic difference with ACSL.
statement ::= /*@ loop-annot */
C-iteration-statement
loop-annot ::= loop-clause ∗ loop-behavior ∗
loop-variant?
loop-clause ::= loop-invariant | loop-assigns
| loop-allocation
loop-invariant ::= clause-kind ?
loop invariant pred ;
loop-assigns ::= loop assigns locations ;
loop-behavior ::= for id (, id)∗ : loop-clause ∗ annotation for behavior id
loop-variant ::= loop variant term ;
| loop variant term for id ; variant for relation id
Figure 2.11: Grammar for loop annotations
loop allocation and loop assigns are usually difficult to implement, since they require the
implementation of a memory model. Thus, most tools may not support them (or may support them
partially).
16
2.4. STATEMENT ANNOTATIONS
Loop invariants
The semantics of loop invariants is the same than the one defined in ACSL, except that they are not
inductive. More precisely, if one does not take care of side effects (the semantics of specifications about
side effects in loop is the same in E-ACSL than the one in ACSL), a loop invariant I is valid in ACSL
if and only if:
– I holds before entering the loop; and
– if I is assumed true in some state where the loop condition c is also true, and if the execution of
the loop body in that state ends normally at the end of the body or with a "continue" statement,
I is true in the resulting state.
In E-ACSL, the same loop invariant I is valid if and only if:
– I holds before entering the loop; and
– if the execution of the loop body in that state ends normally at the end of the body or with a
"continue" statement, I is true in the resulting state.
Thus the only difference with ACSL is that E-ACSL does not assume that the invariant previously
holds when one checks that it holds at the end of the loop body. In other words a loop invariant I is
equivalent to putting an assertion I just before entering the loop and at the very end of the loop body.
Example 2.8 In the following, bsearch(t,n,v) searches for element v in array t between indices
0 and n-1.
/*@ requires n >= 0 && \valid(t+(0..n-1));
@ assigns \nothing;
@ ensures -1 <= \result <= n-1;
@ behavior success:
@ ensures \result >= 0 ==> t[\result] == v;
@ behavior failure:
@ assumes t_is_sorted : \forall integer k1, int k2;
@ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];
@ ensures \result == -1 ==>
@ \forall integer k; 0 <= k < n ==> t[k] != v;
@*/
int bsearch(double t[], int n, double v) {
int l = 0, u = n-1;
/*@ loop invariant 0 <= l && u <= n-1;
@ for failure: loop invariant
@ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
@*/
while (l <= u ) {
int m = l + (u-l)/2; // better than (l+u)/2
if (t[m] < v) l = m + 1;
else if (t[m] > v) u = m - 1;
else return m;
}
return -1;
}
In E-ACSL, this annotated function is equivalent to the following one since loop invariants are not
inductive.
/*@ requires n >= 0 && \valid(t+(0..n-1));
@ assigns \nothing;
@ ensures -1 <= \result <= n-1;
17
2.4. STATEMENT ANNOTATIONS
@ behavior success:
@ ensures \result >= 0 ==> t[\result] == v;
@ behavior failure:
@ assumes t_is_sorted : \forall integer k1, int k2;
@ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];
@ ensures \result == -1 ==>
@ \forall integer k; 0 <= k < n ==> t[k] != v;
@*/
int bsearch(double t[], int n, double v) {
int l = 0, u = n-1;
/*@ assert 0 <= l && u <= n-1;
@ for failure: assert
@ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
@*/
while (l <= u ) {
int m = l + (u-l)/2; // better than (l+u)/2
if (t[m] < v) l = m + 1;
else if (t[m] > v) u = m - 1;
else return m;
/*@ assert 0 <= l && u <= n-1;
@ for failure: assert
@ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
@*/ ;
}
return -1;
}
General inductive invariant
The syntax of this kind of invariant is shown Figure 2.12.
assertion ::= /*@ clause-kind ? invariant pred ; */
| /*@ for id (, id)∗ : clause-kind ? invariant pred ; */
Figure 2.12: Grammar for general inductive invariants
In E-ACSL, a general inductive invariant may be written everywhere in a loop body, and is exactly
equivalent to writing an assertion.
2.4.3 Built-in construct \at
No difference with ACSL, but no forward references.
The construct \at(t,id) (where id is a regular C label, a label added within a ghost statement
or a default logic label) follows the same rule than its ACSL counterpart, except that a more restrictive
scoping rule must be respected in addition to the standard ACSL scoping rule:
– when evaluating \at(t,id) at a propram point p, the program point p′ denoted by id must be
reached before p in the program execution flow; and
– when evaluating \at(t,id), for each C left-value x that contributes to the definition of a (non-
ghost) logic variable involved in t, the equality \at(x,id) == \at(x,Here) must hold, i.e.
the value of x must not be modified between the program points id and Here.
18
2.4. STATEMENT ANNOTATIONS
Below, the first example illustrates the first constraint, whereas the second example illustrates the
second constraint.
Example 2.9 In the following example, both assertions are accepted and valid in ACSL, but only the
first one is accepted and valid in E-ACSL since evaluating the term \at(*(p+\at(*q,Here)),L1)
at L2 requires to evaluate the term \at(*q,Here) at L1: that is forbidden since L1 is executed before
L2.
/*@ requires \valid(p+(0..1));
@ requires \valid(q);
@*/
void f(int *p, int *q) {
*p = 0;
*(p+1) = 1;
*q = 0;
L1: *p = 2;
*(p+1) = 3;
*q = 1;
L2:
/*@ assert (\at(*(p+\at(*q,L1)),Here) == 2); */
/*@ assert (\at(*(p+\at(*q,Here)),L1) == 1); */
return ;
}
Example 2.10 In the following example, the first assertion is supported, while the second one is not
supported. Indeed, in the second assertion, the guard defining the logic variable u depends on n whose
value is modified between L1 and L2.
main(void) {
int m = 2;
int n = 7;;
L1: ;
n = 4;
L2:
/*@ assert
\let k = m + 1;
\exists integer u; 9 <= u < 21 &&
\forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
\at(n + u + v > 0, K); */ ;
/*@ assert
\let k = m + 1;
\exists integer u; n <= u < 21 && // [u] depends on [n]
\forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
\at(n + u + v > 0, L1); */ ;
return 0;
}
Any \at construct involving a logic variable whose definition depends on a C variable is currently
unsupported by plug-in E-ACSL.
Example 2.11 The \old construct (special case of \at) of the following example is not yet supported
since the guard of the quantified variable i depends on the C variable n in the definition of its upper
bound.
19
2.5. TERMINATION
/*@ ensures \forall int i; 0 <= i < n-1 ==> \old(t[i]) == t[i+1]; */
void reverse(int *t, int n);
2.4.4 Statement contracts
No difference with ACSL.
Figure 2.13 shows the grammar of statement contracts.
statement ::= /*@ statement-contract */ statement
statement-contract ::= (for id (, id)∗ :)? requires-clause ∗
simple-clause-stmt∗ named-behavior-stmt∗
completeness-clause ∗
simple-clause-stmt ::= simple-clause | abrupt-clause-stmt
named-behavior-stmt ::= behavior id : behavior-body-stmt
behavior-body-stmt ::= assumes-clause ∗
requires-clause ∗ simple-clause-stmt∗
Figure 2.13: Grammar for statement contracts
2.5 Termination
No difference with ACSL, but no terminates clauses.
2.5.1 Integer measures
No difference with ACSL.
2.5.2 General measures
No difference with ACSL.
2.5.3 Recursive function calls
No difference with ACSL.
2.5.4 Non-terminating functions
No such feature in E-ACSL: whether a function is guaranteed to terminate if some predicate p holds is
not a monitorable property.
2.6 Logic specifications
No difference with ACSL.
Figure 2.14 presents the grammar of logic definitions.
20
2.6. LOGIC SPECIFICATIONS
C-external-declaration ::= /*@ logic-def + */
logic-def ::= logic-const-def
| logic-function-def
| logic-predicate-def
| lemma-def
| data-inv-def
type-var ::= id
type-expr ::= type-var type variable
| id
< type-expr
(, type-expr)∗ > polymorphic type
type-var-binders ::= < type-var
(, type-var)∗ >
poly-id ::= id type-var-binders polymorphic object identifier
logic-const-def ::= logic
type-expr poly-id
= term ;
logic-function-def ::= logic
type-expr
poly-id parameters
= term ;
logic-predicate-def ::= predicate
poly-id parameters ?
= pred ;
parameters ::= ( parameter
(, parameter)∗ )
parameter ::= type-expr id
lemma-def ::= clause-kind ?
lemma poly-id :
pred ;
Figure 2.14: Grammar for global logic definitions
21
2.6. LOGIC SPECIFICATIONS
2.6.1 Predicate and function definitions
No difference with ACSL.
2.6.2 Lemmas
No difference with ACSL.
Lemmas are verified before running the function main but after initializing global variables.
2.6.3 Inductive predicates
Experimental
No difference with ACSL.
Figure 2.15 presents the grammar of inductive predicates.
logic-def ::= inductive-def
inductive-def ::= inductive
poly-id parameters ? { indcase ∗ }
indcase ::= case poly-id : pred ;
Figure 2.15: Grammar for inductive predicates
Inductive predicates in all their generality are not monitorable. Therefore, future versions of this
document will restrict them syntactically (e.g., to definite Horn clauses (http://en.wikipedia.
org/wiki/Horn_clause) and/or through semantic criteria.
2.6.4 Axiomatic definitions
Experimental
No difference with ACSL.
Figure 2.16 presents the grammar of axiomatic definitions.
Axiomatic definitions in all their generality are not monitorable. Therefore, future versions of this
document will restrict them syntactically and/or through semantic criteria.
2.6.5 Polymorphic logic types
No difference with ACSL.
2.6.6 Recursive logic definitions
No difference with ACSL.
2.6.7 Higher-order logic constructions
Experimental
No difference with ACSL.
Figure 2.17 introduces new term constructs for higher-order logic.
Abstractions are only implemented for extended quantifiers, such as the term
\sum(1, 10, \lambda integer k; k).
22
2.6. LOGIC SPECIFICATIONS
logic-def ::= axiomatic-decl
axiomatic-decl ::= axiomatic id { logic-decl ∗ }
logic-decl ::= logic-def
| logic-type-decl
| logic-const-decl
| logic-predicate-decl
| logic-function-decl
| axiom-def
logic-type-decl ::= type logic-type ;
logic-type ::= id
| id type-var-binders polymorphic type
logic-const-decl ::= logic type-expr poly-id ;
logic-function-decl ::= logic type-expr
poly-id parameters ;
logic-predicate-decl ::= predicate
poly-id parameters ? ;
axiom-def ::= axiom poly-id : pred ;
Figure 2.16: Grammar for axiomatic declarations
term ::= \lambda binders ; term abstraction
| ext-quantifier ( term , term , term )
| { term \with [ range ] = term }
ext-quantifier ::= \max | \min | \sum
| \product | \numof
Figure 2.17: Grammar for higher-order constructs
23
2.6. LOGIC SPECIFICATIONS
2.6.8 Concrete logic types
Experimental
No difference with ACSL.
Figure 2.18 introduces new constructs for defining logic types and the associated new terms.
logic-def ::= type logic-type =
logic-type-def ;
logic-type-def ::= record-type
| sum-type
| product-type
| function-type
| type-expr type abbreviation
record-type ::= { type-expr id
( ; type-expr id)∗ ;? }
function-type ::= ( ( type-expr
(, type-expr )∗ )? )
-> type-expr
sum-type ::= |? constructor
( | constructor)∗
constructor ::= id constant constructor
| id
( type-expr
(, type-expr)∗ ) non-constant constructor
product-type ::= ( type-expr
(, type-expr)+ ) product type
term ::= term . id record field access
| \match term
{ match-cases } pattern-matching
| ( term (, term)+ ) tuples
| { (. id = term ;)+ } records
| \let ( id (, id)+ ) =
term ; term
match-cases ::= match-case +
match-case ::= case pat : term
pat ::= id constant constructor
| id ( pat ( , pat)∗ ) non-constant constructor
| pat | pat or pattern
| _ any pattern
| literal | { (. id = pat)∗ } record pattern
| ( pat ( , pat )∗ ) tuple pattern
| pat as id pattern binding
Figure 2.18: Grammar for concrete logic types and pattern-matching
24
2.7. POINTERS AND PHYSICAL ADRESSING
2.6.9 Hybrid functions and predicates
No difference with ACSL.
Hybrid functions and predicates are usually difficult to implement, since they require the implementa-
tion of a memory model (or at least to support \at). Thus, most tools may not support them (or may
support them partially).
2.6.10 Memory footprint specification: reads clause
Experimental
No difference with ACSL.
Figure 2.19 introduces reads clauses.
logic-function-decl ::= logic type-expr poly-id
parameters reads-clause ;
logic-predicate-decl ::= predicate poly-id
parameters ? reads-clause ;
reads-clause ::= reads locations
logic-function-def ::= logic type-expr poly-id
parameters reads-clause = term ;
logic-predicate-def ::= predicate poly-id
parameters ? reads-clause = pred ;
Figure 2.19: Grammar for logic declarations with reads clauses
read clauses are usually difficult to implement, since they require the implementation of a memory
model. Thus, most tools may not support them (or may support them partially).
2.6.11 Specification Modules
No difference with ACSL.
2.7 Pointers and physical adressing
No difference with ACSL.
Figure 2.20 shows the additional constructs for terms and predicates which are related to memory
location.
2.7.1 Memory blocks and pointer dereferencing
No difference with ACSL.
All memory-related built-in functions and predicates are usually difficult to implement, since they
require the implementation of a memory model. Thus, most tools may not support them (or may support
them partially).
2.7.2 Separation
No difference with ACSL.
\separated is usually difficult to implement, since it requires the implementation of a memory
model. Thus, most tools may not support it (or may support it partially).
25
2.8. SETS AND LISTS
term ::= \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 ? ( locations-list )
| \valid_read one-label ? ( locations-list )
| \separated ( location , locations-list )
| \object_pointer one-label ? ( locations-list )
| \pointer_comparable one-label ? ( term , term )
one-label ::= { label-id }
two-labels ::= { label-id, label-id }
Figure 2.20: Grammar extension of terms and predicates about memory
2.7.3 Dynamic allocation and deallocation
No difference with ACSL.
All these constructs are usually difficult to implement, since they require the implementation of a
memory model. Thus, most tools may not support them (or may support them partially).
Figure 2.21 introduces grammar for dynamic allocations and deallocations.
allocation-clause ::= allocates dyn-allocation-addresses ;
| frees dyn-allocation-addresses ;
loop-allocation ::= loop allocates dyn-allocation-addresses ;
| loop frees dyn-allocation-addresses ;
dyn-allocation-addresses ::= locations
Figure 2.21: Grammar for dynamic allocations and deallocations
2.8 Sets and lists
2.8.1 Finite sets
No difference with ACSL.
2.8.2 Finite lists
No difference with ACSL.
Figure 2.22 shows the notations for built-in lists.
26
2.9. ABRUPT TERMINATION
term ::= [| |] empty list
| [| term (, term)∗ |] list of elements
| term ^ term list concatenation (overloading bitwise-xor
operator)
| term *^ term list repetition
Figure 2.22: Notations for built-in list datatype
2.9 Abrupt termination
No difference with ACSL.
Figure 2.23 shows the grammar of abrupt terminations.
abrupt-clause ::= exits-clause
exits-clause ::= exits pred ;
abrupt-clause-stmt ::= breaks-clause | continues-clause | returns-clause
exits-clause
breaks-clause ::= breaks pred ;
continues-clause ::= continues pred ;
returns-clause ::= returns pred ;
term ::= \exit_status
Figure 2.23: Grammar of contracts about abrupt terminations
2.10 Dependencies information
Experimental
No difference with ACSL.
Figure 2.24 shows the grammar for dependencies information.
assigns-clause ::= assigns locations-list (\from locations )? ;
| assigns term \from locations = term ;
Figure 2.24: Grammar for dependencies information
2.11 Data invariants
No difference with ACSL.
Figure 2.25 summarizes grammar for declarations of data invariants.
strong invariants are unlikely evaluated efficiently at runtime.
27
2.12. GHOST VARIABLES AND STATEMENTS
data-inv-def ::= data-invariant | type-invariant
data-invariant ::= inv-strength? global invariant
id : pred ;
type-invariant ::= inv-strength? type invariant
id ( C-type-name id ) = pred ;
inv-strength ::= weak | strong
Figure 2.25: Grammar for declarations of data invariants
2.11.1 Semantics
No difference with ACSL.
2.11.2 Model variables and model fields
No difference with ACSL.
Figure 2.26 summarizes the grammar for declarations of model variables and fields.
logic-def ::= model parameter ; model variable
| model C-type-name { parameter ;? } ; model field
Figure 2.26: Grammar for declarations of model variables and fields
2.12 Ghost variables and statements
No difference with ACSL.
Figure 2.27 summarizes the grammar for ghost statements which is the same than the one of ACSL.
2.12.1 Volatile variables
Figure 2.28 summarizes the grammar for volatile constructs.
2.13 Initialization and undefined values
No difference with ACSL.
\initialized is usually difficult to implement, since it requires the implementation of a memory
model. Thus, most tools may not support it (or may support it partially).
The Frama-C plug-in E-ACSL does not support labels as arguments of \initialized.
2.14 Dangling pointers
No difference with ACSL.
28
2.14. DANGLING POINTERS
C-type-qualifier ::= \ghost only in ghost
C-type-specifier ::= logic-type
logic-def ::= ghost C-declaration
C-direct-declarator ::= C-direct-declarator function declarator
( C-parameter-type-list?
) /*@ ghost (
C-parameter-type-list with ghost params
) */
C-postfix-expression ::= C-postfix-expression function call
( C-argument-expression-list?
) /*@ ghost (
C-argument-expression-list with ghost args
)
*/
C-statement ::= /*@ ghost
C-statement+ ghost code
*/
| if ( C-expression )
statement
/*@ ghost
else C-statement ghost alternative
C-statement∗ unconditional ghost code
*/
C-struct-declaration ::= /*@ ghost
C-struct-declaration ghost field
*/
Figure 2.27: Grammar for ghost statements
logic-def ::= //@ volatile locations (reads ident)? (writes ident)? ;
Figure 2.28: Grammar for volatile constructs
29
2.15. WELL-TYPED POINTERS
\dangling is usually difficult to implement, since it requires the implementation of a memory
model. Thus, most tools may not support it (or may support it partially).
2.15 Well-typed pointers
No such feature in E-ACSL: it would require the implementation of a C type system at runtime.
2.16 Logic attribute annotations
No such feature in E-ACSL: logic attributes are implementation dependent; therefore their meaning
cannot be guessed by a general-purpose (runtime) verification tool.
2.17 Preprocessing for ACSL
No difference with ACSL.
30
Libraries 3
Disclaimer: this chapter is empty on purpose. It is left here to be consistent with the ACSL reference
manual [2].
31
Conclusion 4
This document presents an Executable ANSI/ISO C Specification Language. It provides a subset of
ACSL [2] implemented [3] in the Frama-C platform [7] in which each construct may be evaluated at
runtime. The specification language described here is intended to evolve in the future in two directions.
First it is based on ACSL which is itself still evolving. Second the considered subset of ACSL may also
change.
32
Appendices A
A.1 Changes
Version 1.19
– Update according to ACSL 1.19
– Section 2.7.1: add the \object_pointer and \pointer_comparable built-in predi-
cates.
Version 1.18
– No changes: changes in ACSL 1.18 do not impact E-ACSL.
Version 1.17
– Section 2.2: xor ^^ is not lazy.
– Section 2.2: new extended syntax for quantifications.
– Section 2.2.5: additional remark about real numbers and operations over them.
– Section 2.3.4: new extended syntax for set comprehensions.
– Section 2.4.3: more restrictive scoping rule for \at constructs.
– Section 2.6: add lemmas and data invariants.
– Section 2.6.3: add inductive predicates experimentally: the accepted subset will be refined in a
future version.
– Section 2.6.4: add axiomatic declarations experimentally: the accepted subset will be refined in
a future version.
– Section 2.6.5: add polymorphic logic types.
– Section 2.6.7: add higher-order logic constructions.
– Section 2.6.8: add concrete logic types.
– Section 2.6.10: add read clauses.
– Section 2.10: add dependencies information.
– Section 2.12.1: add volatile constructs.
Version 1.16
– Update according to ACSL 1.16
– Section 2.3: add the check and admit clause kinds.
– Section 2.4.1: add the check and admit clause kinds.
– Section 2.4.2: add the check and admit clause kinds.
– Section 2.4.2: add the check and admit clause kinds.
33
A.1. CHANGES
Version 1.15
– Update according to ACSL 1.15:
– Section 2.12: add the \ghost qualifier.
Version 1.14
– Update according to ACSL 1.14:
– Section 2.4.1: add the keyword check.
Version 1.13
– Update according to ACSL 1.13:
– Section 2.3.4: add syntax for set membership.
Version 1.12
– Update according to ACSL 1.12:
– Section 2.3.4: add subsections for build-in lists.
– Section 2.4.4: fix syntax rule for statement contracts in allowing completeness clauses.
– Section 2.7.1: add syntax for defining a set by giving explicitly its element.
– Section 2.15: new section.
Version 1.9
– Section 2.7.3: new section.
– Update according to ACSL 1.9.
Version 1.8
– Section 2.3.4: fix example 2.6.
– Section 2.7: add grammar of memory-related terms and predicates.
Version 1.7
– Update according to ACSL 1.7.
– Section 2.7.2: no more absent.
Version 1.5-4
– Fix typos.
– Section 2.2: fix syntax of guards in iterators.
– Section 2.2.2: fix definition of undefined terms and predicates.
– Section 2.2.3: no user-defined types.
– Section 2.3.1: no more implementation issue for \old.
– Section 2.4.3: more restrictive scoping rule for label references in \at.
Version 1.5-3
– Fix various typos.
– Warn about features known to be difficult to implement.
– Section 2.2: fix semantics of ternary operator.
34
A.2. CHANGES IN E-ACSL IMPLEMENTATION
– Section 2.2: fix semantics of cast operator.
– Section 2.2: improve syntax of iterator quantifications.
– Section 2.2.2: improve and fix example 2.4.
– Section 2.4.2: improve explanations about loop invariants.
– Section 2.6.9: add hybrid functions and predicates.
Version 1.5-2
– Section 2.2: remove laziness of operator <==>.
– Section 2.2: restrict guarded quantifications to integer.
– Section 2.2: add iterator quantifications.
– Section 2.2: extend unguarded quantifications to char.
– Section 2.3.4: extend syntax of set comprehensions.
– Section 2.4.2: simplify explanations for loop invariants and add example..
Version 1.5-1
– Fix many typos.
– Highlight constructs with semantic changes in grammars.
– Explain why unsupported features have been removed.
– Indicate that experimental ACSL features are unsupported.
– Add operations over memory like \valid.
– Section 2.2: lazy operators &&, ||, ^^, ==> and <==>.
– Section 2.2: allow unguarded quantification over boolean.
– Section 2.2: revise syntax of \exists.
– Section 2.2.2: better semantics for undefinedness.
– Section 2.3.4: revise syntax of set comprehensions.
– Section 2.4.2: add loop invariants, but they lose their inductive ACSL nature.
– Section 2.5.2: add general measures for termination.
– Section 2.6.11: add specification modules.
Version 1.5-0
– Initial version.
A.2 Changes in E-ACSL Implementation
Version Cobalt-27.1
– Section 2.6.7: support for \sum, \prod, and \numof.
Version Vanadium-23
– Section 2.2: mark logic function and predicate applications as implemented.
– Section 2.3: support for admit and check clauses.
– Section 2.4.2: support for loop variants.
Version Titanium-22
– Section 2.2: support for bitwise operations.
– Section 2.2.7: support for logic arrays.
35
A.2. CHANGES IN E-ACSL IMPLEMENTATION
Version Scandium-21
– Section 2.2.5: support for rational numbers and operations.
– Section 2.3: remove abrupt clauses from the list of exceptions.
– Section 2.3: support for complete behaviors and disjoint behaviors.
– Section 2.4.4: remove abrupt clauses from the list of exceptions.
– Section 2.9: add grammar for abrupt termination.
Version Potassium-19
– Section 2.6: support for logic functions and predicates.
Version Argon-18
– Section 2.4.3: support for \at on purely logic variables.
– Section 2.3.4: support for ranges in memory built-ins (e.g. \valid or \initialized).
Version Chlorine-20180501
– Section 2.2: support for \let binding.
Version 0.5
– Section 2.7.3: support for \freeable.
Version 0.3
– Section 2.4.2: support for loop invariant.
Version 0.2
– Section 2.2: support for bitwise complementation.
– Section 2.7.1: support for \valid.
– Section 2.7.1: support for \block_length.
– Section 2.7.1: support for \base_addr.
– Section 2.7.1: support for \offset.
– Section 2.14: support for \initialized.
Version 0.1
– Initial version.
36
Bibliography
[1] Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, and Allan Blanchard. Wp
Plug-in Manual. https://frama-c.com/fc-plugins/wp.html.
[2] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick
Moy, and Virgile Prevosto. ACSL, ANSI/ISO C Specification Language. https://frama-c.
com/html/acsl.html.
[3] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick
Moy, and Virgile Prevosto. ACSL, Implementation in Frama-C. https://frama-c.com/
download/frama-c-acsl-implementation.pdf.
[4] David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre, André Maroneze, Valentin
Perelle, and Virgile Prevosto. Eva — The Evolved Value Analysis Plug-in. https://frama-c.
com/fc-plugins/eva.html.
[5] Patrice Chalin. Reassessing JML’s logical foundation. In Proceedings of the 7th Workshop on
Formal Techniques for Java-like Programs (FTfJP’05), Glasgow, Scotland, July 2005.
[6] Patrice Chalin. A sound assertion semantics for the dependable systems evolution verifying compiler.
In Proceedings of the International Conference on Software Engineering (ICSE’07), pages 23–33,
Los Alamitos, CA, USA, 2007. IEEE Computer Society.
[7] Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, Virgile Prevosto, Armand
Puccetti, Julien Signoles, and Boris Yakobowski. Frama-C User Manual. https://frama-c.
com/download/frama-c-user-manual.pdf.
[8] International Organization for Standardization (ISO). The ANSI C standard (C99). http:
//www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf.
[9] Brian Kernighan and Dennis Ritchie. The C Programming Language (2nd Ed.). Prentice-Hall, 1988.
[10] Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and
tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota,
pages 105–106, 2000.
[11] Julien Signoles, Basile Desloges, and Kostyantyn Vorobyov. Frama-C’s E-ACSL Plug-in. https:
//frama-c.com/fc-plugins/e-acsl.html.
37
List of Figures
1.1 Summary of not-yet-implemented features. . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.1 Grammar of terms. The terminals id, C-type-name, and various literals are the same as
the corresponding C lexical tokens. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.2 Grammar of predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.3 Grammar of binders and type expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.4 Grammar of guarded quantifications. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.5 Grammar of iterator declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.6 Operator precedence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.7 Grammar of function contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.8 \old and \result in terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.9 Grammar for sets of terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.10 Grammar for assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.11 Grammar for loop annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.12 Grammar for general inductive invariants . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.13 Grammar for statement contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.14 Grammar for global logic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.15 Grammar for inductive predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.16 Grammar for axiomatic declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.17 Grammar for higher-order constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.18 Grammar for concrete logic types and pattern-matching . . . . . . . . . . . . . . . . . . 24
2.19 Grammar for logic declarations with reads clauses . . . . . . . . . . . . . . . . . . . . . 25
2.20 Grammar extension of terms and predicates about memory . . . . . . . . . . . . . . . . 26
2.21 Grammar for dynamic allocations and deallocations . . . . . . . . . . . . . . . . . . . . 26
2.22 Notations for built-in list datatype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.23 Grammar of contracts about abrupt terminations . . . . . . . . . . . . . . . . . . . . . . 27
2.24 Grammar for dependencies information . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.25 Grammar for declarations of data invariants . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.26 Grammar for declarations of model variables and fields . . . . . . . . . . . . . . . . . . . 28
2.27 Grammar for ghost statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.28 Grammar for volatile constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
38
Index
?, 7, 8 for, 13, 15, 17, 19
_, 9, 23 \forall, 8, 9
\freeable, 25
abrupt termination, 26 frees, 25
admit, 13 \fresh, 25
\allocable, 25 \from, 26
allocates, 25 function behavior, 14
\allocation, 25 function contract, 12
annotation, 15
as, 23 ghost, 27
assert, 15 ghost, 28
assigns, 13, 15, 26 \ghost, 28
assumes, 13 global, 27
\at, 17 global invariant, 26
axiom, 22 grammar entries
axiomatic, 22 C-compound-statement, 15
C-direct-declarator, 28
\base_addr, 25 C-external-declaration, 20
behavior, 14 C-postfix-expression, 28
behavior, 13, 19 C-statement, 15, 28
behaviors, 13 C-struct-declaration, 28
\block_length, 25 C-type-qualifier, 28
boolean, 9 C-type-specifier, 28
breaks, 26 abrupt-clause-stmt, 26
abrupt-clause, 26
case, 21, 23 allocation-clause, 25
check, 13 assertion-kind, 15
complete, 13 assertion, 15, 17
continues, 26 assigns-clause, 13, 26
contract, 12, 19 assumes-clause, 13
data invariant, 26 axiom-def, 22
decreases, 13 axiomatic-decl, 22
\decreases, 19 behavior-body-stmt, 19
disjoint, 13 behavior-body, 13
bin-op, 7
else, 28 binders, 9
\empty, 14 binder, 9
ensures, 13 breaks-clause, 26
\exists, 8, 9 built-in-logic-type, 9
\exit_status, 26 clause-kind, 13
exits, 26 completeness-clause, 13
constraints, 14
\false, 7, 8 constructor, 23
39
INDEX
continues-clause, 26 parameters, 20
data-inv-def, 27 parameter, 20
data-invariant, 27 pat, 23
declaration, 9 poly-id, 7, 20
decreases-clause, 13 predicates, 9
dyn-allocation-addresses, 25 pred, 8, 13, 14, 25
ensures-clause, 13 product-type, 23
exits-clause, 26 range, 14
ext-quantifier, 22 reads-clause, 24
function-contract, 13 record-type, 23
function-type, 23 rel-op, 8
guard-op, 9 requires-clause, 13
guarded-quantif, 9 returns-clause, 26
guards, 9 simple-clause-stmt, 19
ident, 7 simple-clause, 13
indcase, 21 statement-contract, 19
inductive-def, 21 statement, 15, 19
integer-guard-op, 8 sum-type, 23
integer-guards, 8 terms, 9
interv, 8, 9 term, 7, 13, 22, 23, 25, 26
inv-strength, 27 tset, 14
iterator-guard, 8, 9 two-labels, 25
iterator, 9 type-expr, 9, 20
lemma-def, 20 type-invariant, 27
literal, 7 type-var-binders, 20
locations-list, 13 type-var, 20
locations, 13 unary-op, 7
location, 13 variable-ident, 9
logic-const-decl, 22 wildcard-param, 9
logic-const-def, 20 guards, 9
logic-decl, 22
logic-def, 20–23, 27, 28 hybrid
logic-function-decl, 22, 24 function, 24
logic-function-def, 20, 24 predicate, 24
logic-predicate-decl, 22, 24
logic-predicate-def, 20, 24 if, 28
logic-type-decl, 22 \in, 14
logic-type-def, 23 inductive, 21
logic-type-expr, 9 inductive predicates, 21
logic-type, 22 integer, 9
loop-allocation, 25 \inter, 14
loop-annot, 15 invariant, 16
loop-assigns, 15 data, 26
loop-behavior, 15 global, 26
loop-clause, 15 type, 26
loop-invariant, 15 invariant, 15, 17, 27
loop-variant, 15 iterator, 9
match-cases, 23
\lambda, 22
match-case, 23
lemma, 20
named-behavior-stmt, 19
\let, 7, 8, 23
named-behavior, 13
location, 25
one-label, 25
logic, 20, 22, 24
40
INDEX
logic specification, 19 volatile, 27, 28
loop, 15, 25
weak, 27
\match, 23 \with, 7, 22
\max, 22 writes, 28
\min, 22
model, 27
model, 27
nexts, 9
\nothing, 13
\null, 25
\numof, 22
\object_pointer, 25
\offset, 25
\old, 13
\pointer_comparable, 25
polymorphism, 21
predicate, 20, 22, 24
\product, 22
reads, 24, 28
real, 9
recursion, 21
requires, 13
\result, 13
returns, 26
\separated, 25
sizeof, 7
specification, 19
statement contract, 19
strong, 27
\subset, 14
\sum, 22
termination, 19
\true, 7, 8
type
concrete, 23
polymorphic, 21
record, 23
sum, 23
type, 22, 23, 27
type invariant, 26
\union, 14
\valid, 25
\valid_read, 25
variant, 15
\variant, 19
41