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.
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.
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.
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).
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:
- array annotations on array pointer variables, parameters and fields
- null annotations on nullable pointer variables, parameters and fields
- preconditions on any functions that take null-terminated strings as parameters
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.
eCv Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.
