Information Technology Reference
In-Depth Information
e-acsl keyword Its semantics
\base_addr
(p)
the base address of the block containing pointer
p
\block_length
(p)
the size (in bytes) of the block containing pointer
p
\offset
(p)
the offset (in bytes) of
p
in its block (i.e., w.r.t.
\base_addr
(p)
)
⎬
is true iff reading
*
p
is safe
\valid_read
(p)
here
p
must be a
non-void pointer
is true iff reading and writing
*
p
is safe
\valid
(p)
⎭
\initialized
(p)
is true iff
*
p
has been initialized
Fig. 1.
Memory-related e-acsl constructs currently supported by e-acsl2c
2 Executable Specifications Require Memory Monitoring
The executable specification language e-acsl [6, 9] was designed to support
runtime assertion checking in Frama-C. Frama-C [5] is a platform dedicated
to analysis of C programs that includes various analyzers, such as abstract in-
terpretation based value analysis (Value plug-in), dependency analysis, pro-
gram slicing, jessie and wp plug-ins for proof of programs, etc. acsl [10] is a
behavioral specification language shared by different Frama-C analyzers that
takes the best of the specification languages of earlier tools Caveat [11] and
Caduceus [12], themselves inspired by JML [13].
acsl is expressive enough to express most functional properties of C pro-
grams and has already been used in many projects, including large-scale indus-
trial ones [5]. It is based on a typed first-order logic in which terms may contain
pure
(
i.e.
side-effect free) C expressions and special keywords. An Eiffel-like
contract [14] may be associated to each function in order to specify its pre- and
postconditions. The contract can be split into several named guarded behaviors.
Contracts may also be associated to statements, as well as assertions, loop invari-
ants and loop variants. acsl annotations also include definitions of (inductive)
predicates, axiomatics, lemmas, logic functions, data invariants and ghost code.
Designed as a large subset of acsl, e-acsl preserves acsl semantics. More-
over, the e-acsl language is
executable
: its annotations can be translated into
C monitors by e-acsl2c and executed at runtime. This makes it suitable for
runtime assertion checking. Fig. 1 presents some memory-related e-acsl an-
notations. We use the term
(memory) block
for any (statically, dynamically or
automatically) allocated object. A block is characterized by its size and its
base
address,
that is, the address of its first byte.
Fig. 2 shows a simple C function
findchr
with an acsl contract (that is also an
e-acsl contract) enclosed into
@
-comments. Given a character
c
and a pointer
s
to an array of
n
characters,
findchr
returns a pointer to an occurrence of
c
in
the array, and
NULL
otherwise. It is very similar to the C standard
memchr
function
(basically, our contract does not require to find the
first
occurrence of
c
). The
contract contains two behaviors (lines 2-6, 7-9) with a common precondition
(line 1). The precondition states that
s
must refer to a valid readable location
with at least
n
characters to the right of
s
. The first behavior
found
is defined by
the
assumes
clause line 3. Whenever the
assumes
condition is satisfied, the behav-
ior's postconditions (lines 4-6) must be ensured. They state that the returned
