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
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
Ensuring validity
Which preprocessor?
Verification
Constructs that are unverifiable
General Notes
Type constraints
Function Contracts
Loop specifications
Ghost declarations
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
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
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.