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:

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:

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:

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:

eCv can only reason about calls to the standard library function memset when at least one of the following is true:

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:

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   TOC

eCv Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.