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

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

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

Verifying your source

Ensuring validity
Which preprocessor?
Verification
Constructs that are unverifiable

Specifications

General Notes
Type constraints
Function Contracts
Loop specifications
Ghost declarations

Additional eCv Constructs

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.