This document describes how VeriFast verifies a .c file. It does so when the .c file is specified as a command-line argument of the verifast command-line tool, or when the .c file is loaded into the VeriFast IDE and the Verify command is issued.
VeriFast first performs preprocessing on the .c file. While doing so, it checks that the expansion of a header file does not depend on macros defined before the inclusion of the header file. That is, it checks that the expansion of header files is context-free. This is part of ensuring the soundness of the verification of C programs consisting of multiple .c files.
The sequence of tokens obtained after preprocessing is called a translation unit. VeriFast then parses the translation unit, checking that it conforms with the grammar shown below.
It then checks well-formedness of the various declarations, and then verifies each function that has a specification. It verifies the functions in the order in which they appear in the translation unit. We detail the well-formedness conditions for the various declarations and we describe the verification of functions below.
translation-unit:
external-declaration
translation-unit external-declaration
external-declaration:
function-definition
declaration
ghost-declaration-block
ghost-declaration-block:
/*@ ghost-declaration-list @*/
ghost-declaration-list:
ghost-declaration
ghost-declaration-list ghost-declaration
ghost-declaration:
inductive-datatype-declaration
fixpoint-function-definition
predicate-declaration
predicate-family-declaration
predicate-family-instance-definition
predicate-constructor-definition
lemma-function-declaration
box-class-declaration
inductive-datatype-declaration:
inductive identifier generic-parametersopt = |opt inductive-datatype-case-list ;
generic-parameters:
< identifier-list >
inductive-datatype-case-list:
inductive-datatype-case-declaration
inductive-datatype-case-list | inductive-datatype-case-declaration
inductive-datatype-case-declaration:
identifier
identifier ( parameter-listopt )
We describe inductive datatypes by example. The declaration
inductive list<t> = nil | cons(t, list<t>);
introduces the generic type name list and generic pure function names nil and cons. For any type T, type list<T> denotes the smallest set that satisfies the following constraints:
nil<T> is an element of the set.v is a value of type T and l is an element of the set, then cons<T>(v, l) is an element of the set.v of type T and element l of the set, nil<T> is distinct from cons<T>(v, l).v1 and v2 of type T and elements l1 and l2 of the set, cons<T>(v1, l1) is equal to cons<T>(v2, l2) only if v1 is equal to v2 and l1 is equal to l2.The inductive datatype declarations of a translation unit may refer to each other. That is, types may be defined by mutual induction. VeriFast checks that each type is well-defined (recursion through positive positions only) and inhabited.
fixpoint-function-definition:
fixpoint function-definition
A fixpoint function definition defines a pure function in one of three ways:
We describe each case by example. The declaration
fixpoint int length<t>(list<t> xs) {
switch (xs) {
case nil: return 0;
case cons(x, xs0): return length(xs0);
}
}
introduces the generic pure function name length by primitive recursion on its argument xs. The body of a fixpoint function defined by primitive recursion must consist solely of a switch statement whose operand is one of the function’s parameters. The type of this parameter (called the inductive parameter) must be an inductive datatype. The body of each case must be of the form return E;. The expression E may call fixpoint functions defined earlier, and it may also recursively call the fixpoint function being defined. In the latter case, the argument supplied for the inductive parameter must be one of the variables bound by the parameter list of the current case. (For example, the recursive call length(xs0) above is allowed because xs0 is a variable bound in the header of the case.
The declaration
fixpoint int abs(int x) { return x < 0 ? -x : x; }
introduces the pure function name abs. The body of a fixpoint function defined non-recursively must be of the form return E; where E calls only fixpoint functions defined earlier.
For fixpoint functions defined by well-founded recursion, see the wf_funcX.c examples.
predicate-declaration:
predicate identifier generic-parametersopt predicate-parameters ;
predicate-keyword identifier generic-parametersopt predicate-parameters = assertion ;
predicate-keyword:
predicate
copredicate
predicate-parameters:
( parameter-list )
( parameter-list ; parameter-list )
predicate-family-declaration:
predicate_family identifier ( parameter-list ) predicate-parameters ;
predicate-family-instance-definition:
predicate_family_instance identifier ( argument-expression-list ) predicate-parameters = assertion ;
predicate-constructor-definition:
predicate_ctor identifier ( parameter-list ) ( parameter-list ) = assertion ;
lemma-function-declaration:
lemma-keyword declaration
lemma-keyword function-definition
lemma-keyword:
lemma
lemma_auto
lemma_auto ( expression )
function-definition:
declaration-specifiers declarator declaration-listopt compound-statement
declaration-list:
declaration
declaration-list declaration
declaration:
declaration-specifiers init-declarator-listopt ;
static_assert-declaration
declaration-specifiers:
storage-class-specifier declaration-specifiersopt
type-specifier declaration-specifiersopt
type-qualifier declaration-specifiersopt
function-specifier declaration-specifiersopt
alignment-specifier declaration-specifiersopt
init-declarator-list:
init-declarator
init-declarator-list , init-declarator
init-declarator:
declarator
declarator = initializer
storage-class-specifier:
typedef
extern
static
_Thread_local
auto
register
type-specifier:
void
char
short
int
long
float
double
signed
unsigned
_Bool
_Complex
atomic-type-specifier
struct-or-union-specifier
enum-specifier
typedef-name
identifier generic-argumentsopt
real
fixpoint ( type-list )
predicate predicate-parameters
any
generic-arguments:
< type-list >
type-list:
type
type-list , type
type:
declaration-specifiers
struct-or-union-specifier:
struct-or-union identifieropt { struct-declaration-list }
struct-or-union identifier
struct-or-union:
struct
union
struct-declaration-list:
struct-declaration
struct-declaration-list struct-declaration
struct-declaration:
specifier-qualifier-list struct-declarator-listopt ;
static_assert-declaration
specifier-qualifier-list:
type-specifier specifier-qualifier-listopt
type-qualifier specifier-qualifier-listopt
alignment-specifier specifier-qualifier-listopt
struct-declarator-list:
struct-declarator
struct-declarator-list , struct-declarator
struct-declarator:
declarator
declaratoropt : constant-expression
enum-specifier:
enum identifieropt { enumerator-list }
enum identifieropt { enumerator-list , }
enum identifier
enumerator-list:
enumerator
enumerator-list , enumerator
enumerator:
enumeration-constant
enumeration-constant = constant-expression
atomic-type-specifier:
_Atomic ( type-name )
type-qualifier:
const
restrict
volatile
_Atomic
function-specifier:
inline
_Noreturn
alignment-specifier:
_Alignas ( type-name )
_Alignas ( constant-expression )
declarator:
pointeropt direct-declarator
direct-declarator:
identifier
( declarator )
direct-declarator [ type-qualifier-listopt assignment-expressionopt ]
direct-declarator [ static type-qualifier-listopt assignment-expression ]
direct-declarator [ type-qualifier-list static assignment-expression ]
direct-declarator [ type-qualifier-listopt * ]
direct-declarator generic-parametersopt ( parameter-type-list ) specification-clausesopt
direct-declarator ( identifier-listopt )
specification-clauses:
specification-clause
specification-clauses specification-clause
specification-clause:
/*@ specification-ghost-clause @*/
specification-ghost-clause
specification-ghost-clause:
nonghost_callers_only
: identifier argumentsopt
requires assertion ;
ensures assertion ;
terminates ;
arguments:
( argument-expression-list )
pointer:
* type-qualifier-listopt
* type-qualifier-listopt pointer
type-qualifier-list:
type-qualifier
type-qualifier-list type-qualifier
parameter-type-list:
parameter-list
parameter-list , ...
parameter-list:
parameter-declaration
parameter-list , parameter-declaration
parameter-declaration:
declaration-specifiers declarator
declaration-specifiers abstract-declaratoropt
identifier-list:
identifier
identifier-list , identifier
type-name:
specifier-qualifier-list abstract-declaratoropt
abstract-declarator:
pointer
pointeropt direct-abstract-declarator
direct-abstract-declarator:
( abstract-declarator )
direct-abstract-declaratoropt [ type-qualifier-listopt assignment-expressionopt ]
direct-abstract-declaratoropt [ static type-qualifier-listopt assignment-expression ]
direct-abstract-declaratoropt [ type-qualifier-list static assignment-expression ]
direct-abstract-declaratoropt [ * ]
direct-abstract_declaratoropt ( parameter-type-listopt )
typedef-name:
identifier
initializer:
assignment-expression
{ initializer-list }
{ initializer-list , }
initializer-list:
designationopt initializer
initializer-list , designationopt initializer
designation:
designator-list =
designator-list:
designator
designator-list designator
designator:
[ constant-expression ]
. identifier
static_assert-declaration:
_Static_assert ( constant-expression , string-literal ) ;
See Shared boxes: rely-guarantee reasoning in VeriFast.
statement:
labeled-statement
compound-statement
expression-statement
selection-statement
iteration-statement
jump-statement
ghost-statement-block
ghost-statement
labeled-statement:
identifier : statement
case constant-expression : statement
case identifier case-argumentsopt : statement
default : statement
compound-statement:
{ block-item-listopt }
block-item-list:
block-item
block-item-list block-item
block-item:
declaration
statement
expression-statement:
expressionopt ;
selection-statement:
if ( expression ) statement
if ( expression ) statement else statement
switch ( expression ) statement
iteration-statement:
while ( expression ) loop-annotations statement
do loop-annotations statement while ( expression ) ;
for ( expressionopt ; expressionopt ; expressionopt ) loop-annotations statement
for ( declaration expressionopt ; expressionopt ) loop-annotations statement
loop-annotations:
loop-annotation
loop-annotations loop-annotation
loop-annotation:
/*@ loop-ghost-annotation @*/
loop-ghost-annotation
loop-ghost-annotation:
invariant assertion ;
requires assertion ;
ensures assertion ;
decreases expression ;
jump-statement:
goto identifier ;
continue ;
break ;
return expressionopt ;
ghost-statement-block:
/*@ ghost-statement @*/
ghost-statement:
open coefficientopt predicate-assertion ;
close coefficientopt predicate-assertion ;
leak assertion ;
invariant assertion ;
produce_lemma_function_pointer_chunk identifier generic-argumentsopt arguments ( identifier-list ) compound-statement statement
duplicate_lemma_function_pointer_chunk ( expression ) ;
produce_function_pointer_chunk identifier generic-argumentsopt ( expression ) arguments ( identifier-list ) compound-statement
merge_fractions assertion ;
shared-boxes-ghost-statements
statement
See Shared boxes: rely-guarantee reasoning in VeriFast.
primary-assertion:
coefficientopt points-to-assertion
coefficientopt predicate-assertion
expression
switch ( expression ) { switch-assertion-case-list }
( assertion )
forall_ ( type identifier ; expression )
emp
coefficient:
[ pattern ]
points-to-assertion:
conditional-expression |-> pattern
predicate-assertion:
identifier generic-argumentsopt patternsopt patterns
patterns:
( pattern-listopt )
pattern-list:
pattern
pattern-list , pattern
pattern:
_
? identifier
identifier patterns
expression
^ expression
switch-assertion-case-list:
switch-assertion-case
switch-assertion-case-list switch-assertion-case
switch-assertion-case:
case identifier case-argumentsopt : return assertion ;
case-arguments:
( identifier-listopt )
assertion:
primary-assertion
primary-assertion &*& assertion
expression ? assertion : assertion
ensures assertion
primary-expression:
identifier generic-argumentsopt
constant
string-literal
( expression )
generic-selection
switch ( expression ) { switch-expression-case-list }
switch-expression-case-list:
switch-expression-case
switch-expression-case-list switch-expression-case
switch-expression-case:
case identifier case-argumentsopt : return expression ;
generic-selection:
_Generic ( assignment-expression , generic-assoc-list )
generic-assoc-list:
generic-association
generic-assoc-list , generic-association
generic-association:
type-name : assignment-expression
default : assignment-expression
postfix-expression:
primary-expression
postfix-expression [ expression ]
postfix-expression ( argument-expression-listopt )
postfix-expression . identifier
postfix-expression -> identifier
postfix-expression ++
postfix-expression -
( type-name ) { initializer-list }
( type-name ) { initializer-list , }
argument-expression-list:
assignment-expression
argument-expression-list , assignment-expression
unary-expression:
postfix-expression
++ unary-expression
- unary-expression
unary-operator cast-expression
sizeof unary-expression
sizeof ( type-name )
_Alignof ( type-name )
unary-operator: one of
& * + - ~ !
cast-expression:
unary-expression
( type-name ) cast-expression
multiplicative-expression:
cast-expression
multiplicative-expression * cast-expression
multiplicative-expression / cast-expression
multiplicative-expression % cast-expression
additive-expression:
multiplicative-expression
additive-expression + multiplicative-expression
additive-expression - multiplicative-expression
shift-expression:
additive-expression
shift-expression << additive-expression
shift-expression >> additive-expression
truncating-expression:
shift-expression
/*@ truncating @*/ postfix-expression
truncating postfix-expression
relational-expression:
truncating-expression
relational-expression < truncating-expression
relational-expression > truncating-expression
relational-expression <= truncating-expression
relational-expression >= truncating-expression
equality-expression:
relational-expression
equality-expression == relational-expression
equality-expression != relational-expression
AND-expression:
equality-expression
AND-expression & equality-expression
exclusive-OR-expression:
AND-expression
exclusive-OR-expression ^ AND-expression
inclusive-OR-expression:
exclusive-OR-expression
inclusive-OR-expression | exclusive-OR-expression
logical-AND-expression:
inclusive-OR-expression
logical-AND-expression && inclusive-OR-expression
logical-OR-expression:
logical-AND-expression
logical-OR-expression || logical-AND-expression
conditional-expression:
logical-OR-expression
logical-OR-expression ? expression : conditional-expression
assignment-expression:
conditional-expression
unary-expression assignment-operator assignment-expression
assignment-operator: one of
= *= /= %= += -= <<= >>= &= ^= |=
expression:
assignment-expression
expression , assignment-expression
constant-expression:
conditional-expression