Verifying your source

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 #define environment, i.e. when parsing a set of files, it need only consider one instance of each header file. So don't use #ifdef, #ifndef or #if 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 command 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 different compilers.

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.

Which preprocessor?

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.

Verification

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 not want 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.

Constructs 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-qualified 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 at least 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 at least 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.

Suppressing verification of included files

Sometimes you may with to suppress verification of certain #include files, for example vendor-supplied include files. eCv maintains a list of the names (with full paths) that you do not wish to verify. There are two ways of adding file names to this list:

By putting the following line in files that you do not wish to be verified:
#pragma ECV noverify
This adds the current file to the do-not-verify list. For all #include directives after the first occurrence of this pragma in a file, those included files will also be added to the do-not-verify list.
By putting the following in a file that contains an #include directive for the file you do not wish to verify, prior to that #include directive:
#pragma ECV noverifyincludefiles #include "file1.h" #include "file2.h" #pragma ECV verifyincludefiles
In this example, file1.h and file2.h are added to the do-not-verify list, as are any files that they #include.

Note: once a file has been added to the do-not verify list, it will never be verified, even if it is also included from another context in which there is no pragma to suppress verification. The Verification Report produced by EscherTool includes a list of files for which verification was suppressed.

TOC