Escher C Verifier (eCv) Reference Manual
Version 5.0, September 2011
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
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
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
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
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++
Appendix F - Grammar of eCv constructs for C
Appendix G - Differences from MISRA C
eCv Manual, Version 5.0, September 2011.
© 2010 onwards Escher Technologies Limited. All rights reserved.