Introduction to Escher C Verifier

eCv is a tool for verifying programs written in a subset of C or C++. Unlike traditional static analysis tools, eCv verifies software so that it is mathematically proven not only to be free from run-time errors, but also to be correct with respect to a well-defined functional specification.

What eCv is intended for

eCv has been designed for developing and verifying critical embedded software. Therefore, eCv requires you to write your program in a safe, type-strengthened subset of C (based on MISRA-C 2004). Constructs that are not suitable for use in safety-critical embedded software - for example, dynamic memory allocation and concurrency - are either not supported at all, or supported only when they are used in certain ways. If you are looking to verify C programs that are not written with safety in mind, then eCv may not be the tool you are looking for.

Because eCv supports only a safe subset of C, the annotation language of eCv is simpler than the annotation language of more general tools, making eCv more suitable for ordinary software developers.

Unlike other formal tools for C, eCv provides a mechanism for expressing high-level software requirements and specifications as well as low-level ones. In support of this, eCv provides abstract data types such as sets and sequences, together with a wide range of operations on them.

We strongly recommend that you use eCv alongside your compiler when developing your software, rather than applying eCv only when development is believed to be complete. Indeed, we suggest running code through eCv in Check mode even before you compile it, to check that your code complies with the eCv safe subset of C. Verifying previously-developed code with eCv is practical only if the source code was written to a high standard and you are prepared to make changes to it.

Principles

eCv uses the Verified Design-by-Contract (VDbC) paradigm and a powerful automatic theorem prover (the same theorem prover as in Escher Technologies' flagship product Perfect Developer). Verified Design-by-Contract builds on the widely-known design-by-contract principle by adding automated proof that contracts are fulfilled or not. All possible violations of contract are detected by eCv prior to compilation. This is clearly preferable to the alternative of hoping that during testing, the test cases used were sufficient to detect all contract violations.

Furthermore, eCv recognizes that many programming language constructs and library functions have implicit contracts; for example, preconditions that are required to hold in order to avoid undefined or implementation-defined behaviour. eCv verifies that these preconditions hold, too.

Preconditions and other specification annotations for eCv are expressed using some additional keywords, with bracketed arguments where needed. When you compile your program using a regular C or C++ compiler, these additional keywords are defined as macros with empty expansions. This means that the specifications are invisible to the compiler, which can still translate your source code as if the specifications were not there.

Programming languages supported by eCv

You can write programs for processing with eCv in subsets of C90, C99, or C++, depending on what compiler you intend to use.

Any program which is a valid eCv program and which is also a valid program in two (or even all three) of those languages has the same meaning in both (all) of them, provided that the compilers you use implement implementation-dependent features of C/C++ in the same way. This makes it easier for you to switch from using a C90 compiler to using a C++ compiler, for example.

Installation and configuration of eCv

Install Escher Verification Studio from the CD or download, ensuring that you include the Escher C Verifier sub-feature.

Load Escher Verification Studio.

Go to Options → Editor and configure eCv to use your preferred editor. Assuming that your editor supports syntax highlighting, we recommend that you also adjust the configuration of the editor itself to highlight the additional eCv language keywords, possibly in a different colour. See here for a list of additional keywords, and the EditorCustomizations subfolder of the Escher Verification Studio installation for preconfigured syntax definition files for some popular editors. If you don't already have an editor that supports syntax highlighting and you are running under Windows, you can find a free editor (Crimson) and an evaluation copy of an inexpensive editor (TextPad) on the Escher C Verifier installation CD.

Optionally, go to Options → C/C++ Compilers and create an entry for each installed C or C++ compiler that your code will be compiled with. See Appendix A for some sample compiler configurations. If a compiler supports different modes (e.g. it can compile in C mode or in C++ mode), or you wish to target more than one platform using the same compiler, you may wish to set up more than one entry for that compiler.

Getting ready to use eCv

File ecv.h is provided with eCv. You will find it in folder "C:\Program Files\Escher Technologies\Verification Studion 5\Escher C Verifier\Include" (replace "C:\Program Files" by your program root directory for 32-bit applications, for example "C:\Program Files (x86)" under 64-bit Windows). You must include a directory that contains ecv.h in your compiler's file include path and in eCv's include path. Either copy ecv.h into the directory where your own standard header file is kept, or configure your development environment or build system to include the installed location of ecv.h in the include file path when you run your compiler(s).

Caution!Each C or C++ source file must directly or indirectly #include file "ecv.h". This inclusion must come before any specifications or other eCv constructs in the source file, and before including other files that contain specifications or other eCv constructs. We recommend that you #include "ecv.h" right at the beginning of one of your own header files (for example, you may already have a header file that defines integral types of fixed sizes taking account of the target platforms), and then #include that file right at the start of every .c file.

Unless you are writing in C++, you also need to set up standard definitions for a Boolean type, or make your existing Boolean type definition understandable to eCv. See the section on Defining and Using Boolean types. We suggest that you put these definitions in the same header file in which you #include "ecv.h".

Depending on your source code, eCv may need to know the definitions of types size_t, ptrdiff_t and (unless your source is C++) wchar_t. These are all defined in the standard header file stddef.h for C90 or C99, or cstddef for C++. Therefore, we suggest that you #include this file in the header file that includes "ecv.h" too.

Setting up your first eCv project

Command line or Project Manager?

eCv may be used from the command line, or from the graphical user interface provided by the Project Manager of Escher Verification Studio. To run eCv from the command line (recommended for advanced users only), you will need to set up a batch file or shell script to invoke EscherTool, optionally passing your C/C++ source code through your compiler's preprocessor first. The command line syntax for EscherTool is given in the Escher Verification Studio User Guide. The remainder of this document assumes that you are using the Project Manager.

To create your first project, first load the Project Manager via the Escher Verification Studio shortcut or the file VerificationStudio.exe. Next, either go to File → New Project or click on the blank-sheet button on the toolbar. If you are asked what sort of files your project will contain, select C/C++ files. Choose a name and folder location for your project.

Adding and creating source files

Each project contains a list of the C/C++ source files that you want eCv to process, along with information about which compiler(s) you will be using. If you have existing C or C++ source files for the project, add them to the project (use File → Add, or the + toolbar button). If you wish to create new source files, use File → Add New, or the *+ toolbar button. Remember that each source file must (directly or indirectly) #include "ecv.h".

Configuring the project settings

At this stage, the only item that it is essential to configure is your choice of C or C++ compiler. Select Project → Settings from the menu, or click on the cog icon in the toolbar. In the Compiler box, select one of the compilers you previously configured, or one of the generic ones that was created for you when Escher C Verifier was installed. In the Additional include paths box, use the Add button to add the path to file ecv.h, or to your own header file that includes ecv.h.

Essential annotations

We suggest that if you added existing source files to the project, you go through them and add at least the following types of annotation before running eCv on them:

When you are writing new source, it is best to add these annotations, along with preconditions and other specifications, as you write the code.

Running your eCv project

Run syntax and semantic checks on all files by pressing the yellow-tick button on the toolbar. You can run checks on individual files by right-clicking on the file in the Project Manager window and selecting Check.

Resolve any error messages by appropriate changes to source and/or header files. See the chapter on Making your source code compatible with eCv. Then you can proceed to Verification.

Further instructions on using the Project Manager, together with instructions on running eCv from the command line, can be found in the Escher Verification Studio User Guide.

TOC   TOC

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