Ensuring that verification is valid for your target environment
You must make sure that eCv and your compiler interpret the source code in the same way. In particular:
- eCv assumes (and does not check) that
header files are always parsed in the same
environment, i.e. when parsing a set of files, it need
only consider one instance of each header file. So don't use
inside a header file to make it do different things depending on which file is including it.
- eCv only sees your program in a state in which __ECV__ is
defined. So don't make parts of your program conditional on whether
__ECV__ is defined, unless you really know what you are doing!
- eCv passes the search paths you configure in your project
and in eCv's global compiler settings to the preprocessor;
project-specific paths first, then compiler-specific ones. Make sure
that when you actually compile the code, the compiler uses exactly the
same search path order, in case there are files with the same
name in different places on the search path.
- Some compilers define additional macros automatically, and
most allow additional macro definitions to be provided on the compiler
line. Add these additional macro definitions to the project settings,
so that eCv sees the same set of macro
definitions as the
compiler (plus the definition of __ECV__, which is added automatically
when you run eCv).
- The meaning of a C program, and therefore the verification
conditions that eCv generates, depends on various
compiler/platform details, such as the sizes of the various integral types and the behaviour of integer
division. You must ensure that the details
you have configured in the eCv Project Manager for
the C/C++ compiler you have told it you are using match the actual compiler you
use. If you intend to compile for more than one platform, you must run eCv
verification separately for each platform, unless you know that the
configuration parameters are the same for all of them. You can set up
multiple configurations in a single project to allow for using
Note: in order to determine the maximum and
minimum values that can be stored in variables of the integral types of C, eCv
assumes that your compiler/platform uses twos-complement representation
of signed integral types, and plain binary representation of unsigned
integral types. If this is not the case, then eCv
may give incorrect results.
When you verify your source files, you can use either eCv or the target compiler to preprocess them,
depending on how you have configured the chosen C or C++ compiler in the Project Manager.
If you choose to let eCv preprocess them, you can use the standard header files supplied with eCv,
or you can attempt to use the standard header files supplied with your compiler.
Here are some guidelines to help you choose:
- The easiest and best approach is usually to use eCv to preprocess the source and use the header files supplied with eCv.
To achieve this, configure the eCv include-file path in the Project Manager. Make sure this path includes the directory containing the standard header files,
but not the directory containing your compiler's standard header files. If you need to have both directories in the include path,
put the eCv header files directory earlier in the path.
- If you wish to use your own compiler to preprocess the source, you must configure the Project Manager to do this for your chosen compiler
(use Options → C/C++ Compilers).
- eCv does not perform MISRA checks relating to use of the preprocessor, when you are not using the eCv preprocessor.
- Although it is possible to use eCv to preprocess files but pick up the header files supplied with your compiler,
this may be problematic for two reasons. First, compiler-supplied header files may use language extensions that cause eCv to fail to parse the file
(although it may be possible to define the associated keywords as null macros so that eCv ignores them).
Second, header files supplied with some compilers (notably gcc) depend on a large number of macros that the preprocessor normally defines,
and you need to accurately replicate these macro definitions in order to ensure the correct behaviour.
- If you use the eCv standard header files,
then only definitions in the C standard library will be available. If your software depends on
non-standard definitions in the header files supplied with your compiler, these will not be available when running eCv.
- The header files supplied with eCv include function contracts. If you do not use these header files then the contracts will mnot be available.
You may therefore need to add contracts to your program for standard library functions, in order that code that calls these functions can be verified.
- If you use your own compiler to preprocess the source, then you can use the platform check program supplied with eCv
to check that the type sizes you have configured in the eCv compiler parameters match the values in the compiler-supplied limits.h file.
- If your compiler's preprocessor does not follow the ISO standard, or if you are using features whose behaviour is undefined
(e.g. multiple # and/or ## tokens in a single macro body such that the meaning depends on the order in which they are evaluated),
then the behaviour of the eCv preprocessor and your compiler's preprocessor
may differ, so that the code verified by eCv is not the same as the code seen by your compiler.
When you have resolved any errors (and, optionally, warnings) produced
by eCv when you Check your program, press
the green-tick button on the toolbar to verify your source. Expect a
lot of verification warnings if you haven't yet annotated your
source code with specifications. Resolve verification errors by adding
preconditions and other specifications.
The sort of specifications you need to add depend on what you
want to verify:
- For functions that you want to verify, you need to write
at least preconditions, writes-clauses and loop invariants. You may
also need to write postconditions, if they are called by other functions
that you want to verify.
- For functions (including library functions) that you do
to verify at the present stage, but which are called from functions
that you do want to verify, you need to write
preconditions, writes-clauses, and sometimes postconditions.
- You may also want to write assertions and postconditions to
describe properties you expect to hold.
- You need only write loop variants where you wish to prove
that a loop terminates.
You can run verification on individual files by right-clicking on the
file in the Project Manager window and selecting Verify.
Note that you don't always have to run a Check before running
a Verify, since Verify will start by checking anyway.
that are unverifiable or compromise verification
eCv is unable to verify code that contains
certain constructs as detailed below. Where the integrity or verification results may be
compromised, eCv will generally issue a warning message.
Casts between pointer types
eCv assumes strong typing, therefore it
cannot verify code that contains casts or implicit conversions between pointers to
different types. The exception is that conversions to void* do not make code unverifiable.
Casting away const
eCv assumes that variables annotated by const
are immutable. Casting away const violates this
assumption. However, if you cast away const so that
you can pass a pointer to a function that takes a non-const
parameter, and the function does not actually write through that
parameter, validity of eCv verification is not affected.
Casting away volatile
eCv tracks the value of non-volatile variables, but not the values of volatile variables.
If you cast a volatile-qualifieed pointer to a non-volatile-qualified pointer,
then the variable tracking performed by eCv will not function correctly, and the integrity of verification is compromised.
Calls to memcpy and memset
eCv can only reason about calls to the standard library function memcpy when one of the following is true:
- The third parameter is zero;
- The first two operands were originally pointers of type T* (prior to being converted to void*) and the third
parameter is equal to sizeof(T);
- The first two operands were originally pointers of type T* array (prior to being converted to void*), they each point to the start
of an array, and the third parameter is an exact multiple of sizeof(T).
eCv can only reason about calls to the standard library function memset when one of the following is true:
- The third parameter is zero;
- The first operand was originally a pointer of type T* (prior to being converted to void*), the second
parameter is zero, and the third parameter is equal to sizeof(T);
- The first operand was originally a pointer of type T* array (prior to being converted to void*) and it points to the start of
an array, the second parameter is zero, and the third parameter is an exact multiple of sizeof(T).
In other cases, the validity of verification results is not affected, but expect eCv to find some veriication conditions unprovable.
Note that using memset to
initialize objects that include pointers and/or floating-point fields
is neither portable nor verifiable by eCv.
This is because the bit patterns used to represent null pointers
and floating-point zeros are implementation-defined, not necessarily all zeros.
eCv Manual, Version 6.0, December 2012.
© 2012 Escher Technologies Limited. All rights reserved.