Escher C Verifier (eCv) Reference Manual

Version 7.0, February 2017

Disclaimer

The information in this publication is given in good faith but may contain errors and omissions. The contents of this document and the specifications of eCv are subject to change without notice.

Contents

1. Getting Started

What eCv is intended for
Principles
Programming languages supported by eCv
Installation and configuration of eCv
Getting ready to use eCv
Setting up your first eCv project
Running your eCv project

2. Making your source code compatible with eCv

Overview
Keywords
Restrictions
Defining and Using Boolean types
Pointers
Assertions and assert.h
Extensions to the C and C++ languages
Common error messages
Line and column coordinates in messages
Suppressing warning messages

3. Verifying your source

Ensuring validity
Which preprocessor?
Verification
Constructs that are unverifiable

4. Specifications

General Notes
Type constraints
Function Contracts
Loop specifications
Ghost declarations

5. Additional eCv Constructs

Additional eCv Declarations
Additional eCv Statements
Additional eCv Expressions

6. Predefined ghost types, functions and fields

Global ghost variables
Global ghost functions
Ghost fields of array pointer types
Ghost fields of the void pointer type
Ghost fields of array types
Ghost member functions of array and sequence types

7. Support for C++ source code in eCv++

Supported and unsupported constructs
Additional eCv++ keywords
Casts in C++ programs
Overloaded functions and ambiguity resolution
Inheritance and final classes
Polymorphic pointers
Constructors
Member functions
Early member functions
Function overriding and hiding
Specifications of overriding functions
Operator declarations
Templates

Appendix A - Compiler Settings

Microsoft Visual C++
gcc

Appendix B - Type system of eCv

Appendix C - Constructs you may see in proof output

Appendix D - Verification condition types

Appendix E - Language extensions for C99 and C++ 2011

C99
C++ 2011

Appendix G - Differences from MISRA-C 2004 and MISRA-C 2012

MISRA-C 2004 guidelines not fully enforced by eCv
eCv rules that are stronger than the MISRA-C 2004 guidelines
MISRA-C 2012 guidelines not fully enforced by eCv
eCv rules that are stronger than the MISRA-C 2012 guidelines

 

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