TOC
Escher C++ Verifier (or eCv++ for short) provides formal verification of programs written in subsets of C++ as defined by the 1998 (ISO 2003) and ISO 2011 standards. The subset is carefully designed to meet the safety requirements of high-integrity projects, for example projects written to meet IEC61508 SIL 3 to 4, or DO-178C DAL A and B. Many C++ constructs are excluded from the subset, and other constructs are included but restricted. Nevertheless, the eCv++ subset of C++ provides several advantages over C, such as encapsulation, information hiding, and object-oriented software development.
The eCv++ subset of C++ was derived by starting from the eCv subset of C and adding only those features of C++ that are well-understood, are unambiguous, introduce little or no risk when they are used, and are of obvious benefit in the context of high-integrity embedded software.
The major features of C++ that are included in the current eCv++ subset are:
Features of C++ that are being considered for a future version of the eCv++ subset are:
Features of C++ that are not supported, and not currently planned to be supported include:
A small number of features from the C++ 2011 ISO standard (C++'11) are supported, even when the compiler type is set to C++'98, as follows:
When processing C++ code, in addition to the keywords listed in Chapter 2 and all the C++'98 keywords (whether supported by eCv++ or not), the following words are treated as keywords:
| Normal keyword | Underlying keyword | Where used | See section |
| early | _ecv_early | Indicates that a member function does not depend on dynamic binding | Early functions |
| final | _ecv_final | Indicates that a class may not be inherited from, or that virtual function may not be overridden in a descendant class | Function overriding and hiding |
| from | _ecv_from | Qualifies the declaration of a pointer or reference to indicate that it may point or refer to a class derived from the one indicated in the type | Polymorphic pointers |
| nullptr | _ecv_nullptr | Null pointer expression | Null pointer expression |
| override | _ecv_override | Indicates that the function being declared overrides an inherted virtual function | Virtual functions |
The final and override keywords have the same meaning in eCv as the corresponding identifiers in C++'11. However, eCv treats them as keywords in all contexts, rather than in certain contexts only as C++'11 does. When the source file is compiled by a C++ compiler that implements an earlier version of the standard, they are defined in ecv.h so as to expand to nothing, which makes them invisible to the compiler. Like other eCv keywords, you can #undef them and use keywords _ecv_final and _ecv_override instead if they conflict with identifiers used in your program.
The nullptr keyword has the same meaning as the corresponding C++'11 keyword. It signifies a null value that can be converted implicitly to any nullable pointer type, but not to an integral type. For your convenience, it is defined in eCv as (0) when you are compiling the source using a compiler that implements an older C++ standard.
When you set the source language to C++, a warning will be generated if you use a C-style cast expression that is not equivalent to a static_cast. You are expected to use reinterpret_cast or const_cast to express these more dangerous types of cast. Example:
int a = 1;
int *pa;
const int c = 2;
unsigned char b;
unsigned char *pb;
b = (unsigned char)a; // OK, cast is equivalent to static_cast
pb = (unsigned char*)&a; // error, need to use reinterpret_cast here
pa = (int*)&c; // error, need to use const_cast here
When a function call is potentially ambiguous because the name of the called function has been overloaded, eCv does not apply the standard C++ disambiguation rules, which are complicated and sometimes give surprising results. Instead, eCv applies the stricter rule that the call must match exactly the argument types of one of the candidate function declarations, with no implicit type conversions required. Otherwise, the call is considered ambiguous and an error is reported. Example:
void foo(const int*, short);
void foo(int*, int);
int i;
...
foo(&i, 1L); // OK in C++, ambiguous in eCv++
eCv++ supports single, public inheritance only. You may declare a class final to indicate to eCv++ that no other class inherits it. This makes verification by eCv++ easier in some cases. Therefore, you are recommended to declare classes final where possible. The syntax used by eCv++ to indicate that a class is final is the same as in C++'11. Example:
class Foo final {
...
};
class Derived final : public Base {
...
};
Given a class Foo, in eCv++ the type Foo* means a pointer to an object of exactly class Foo. If you wish to declare a pointer that may point to Foo or any class derived from Foo, then you must qualify the pointer declaration with the eCv++ keyword from. If the pointer is also declared nullable, then from precedes null in the declaration. Here are some examples:
class AbstractBase {
public:
virtual int foo(int) = 0; // Pure virtual function declared, so AbstractBase is an abstract class
};
class ConcreteBase {
public:
virtual int foo(int);
};
class Derived1 : public AbstractBase {
public:
int foo(int) override; // Overrides the only pure virtual function, so Derived is a concrete class
};
class Derived2 : public ConcreteBase {
public:
int foo1(int) override;
};
AbstractBase* pa1; // Error, there can be no objects exactly of type AbstractBase
AbstractBase* from pa2; // OK, pa2 may point to objects of types derived from AbstractBase
ConcreteBase* pc1; // OK, pc1 may point to objects whose type is exactly ConcreteBase
ConcreteBase* from null pc2; // OK, pc2 may be null or point to objects whose type is or is derived from ConcreteBase
Within the specification and body of a nonstatic non-const member function of a class C, the type of the this pointer is C* from unless C is declared final, in which case it is just C*. For const nonstatic member functions, the type of this is const C* from if C is not declared final, and const C* if it is. Within the body of a constructor of class C, the type of *this is always C* whether or not C is declared final.
A constructor must initialize all fields of *this. If a constructor is declared with a writes-clause, you should not include *this in the writes-clause, because it is implicitly assumed. However, any other variables (including static class member variables) directly or indirectly written by a constructor must be mentioned in its writes-clause.
A constructor declared without a writes-clause is assumed to write its non-const pointer parameters according to the same rules as for global and static functions, as well as *this. Therefore, if a constructor takes a non-const pointer parameter that is used only to initialize member data, you should specify writes() to indicate that it does not write to the object addressed by the parameter.
If a constructor is defined with an empty body, then the constructor postcondition will be inferred from the base and member initializers. You may provide an explicit postcondition instead if you prefer, for example to allow you to specify both the state achieved by the initializers and some additional properties of the state that you expect to hold. If the body is not empty, no postcondition is inferred.
Member initializers must be specified in the same order in which the members are declared. This is so that any side-effects of the initializers will occur in left-to-right order.
A constructor may not call any nonstatic member functions of the current class or its bases other than functions declared early (see Early member functions). A constructor may not pass this to any function it calls, other than implicitly to an early member function of the same class or a base class.
Any constructor that can be called with no arguments (a 'default constructor') may not have side-effects. For example, it may not modify static or global variables, or static variables of any class (including its own).
Any constructor that can be called with exactly one argument must be declared explicit. This is to prevent such constructors from introducing new implicit type conversions.
If a nonstatic member function has an explicit writes-clause, then just as with a non-member function, you must specify in the writes clause everything that it directly or indirectly modifies - including any parts of *this. You may include *this in the writes clause, or just some member variables as required. If a nonstatic member function has no writes-clause, then it is assumed to write through any non-const pointer parameters (as for a non-member function), and if the function is not declared const then it is also assumed to write *this.
A non-virtual nonstatic member function may be declared early to indicate that it does not depend on dynamic binding. An early function may not call any other member functions other than early functions, and may not store the this-pointer in any non-local variables, nor pass it as a parameter to another function. Example:
class Base {
int m_x, m_y;
public:
virtual int foo1(int) = 0;
int foo2(int) early {
m_x = 0; // OK
foo1(); // Error - call to non-early function not allowed
}
int foo3(int) const early {
return m_x + m_y; // OK
}
};
Taken together, these restrictions ensure that the result of calling an early function does not depend on dynamic binding of the this-pointer. This means that early functions may safely be called from constructors and invariant declarations.
If a class is declared final, or it has no direct or inherited virtual member functions, or all its virtual member functions have been declared final, then all the member functions of that class cannot depend on dynamic binding of this and are therefore implicitly early.
Within the declaration of a derived class, whenever you override a virtual function inherited from the parent class, you must indicate your intention to override the inherited member using the override keyword. Declaring the overriding member virtual as well is not necessary but is permitted. You may also indicate that the function is not overridden in any child of the current class using the final keyword. eCv++ does not allow you to declare a member in a derived class that hides a non-virtual member of the same name in a base class.
The syntax for using override and final is the same as in C++'11. Here are some examples:
class Base {
public:
virtual int foo1(int);
virtual int foo2(int);
virtual int foo3(int) const;
int foo4(int);
};
class Derived : public Base {
public:
int foo1(int); // Error, missing 'override'
int foo2(int) override; // OK
int foo3(int) const override final; // OK
int foo4(int); // Error, hides foo4(int) in class Base
};
Where a function overrides a virtual function inherited from a base class, there are restrictions on its specification, as follows:
In short, an overriding function may weaken the precondition and/or strengthen the postcondition of the overridden function. Taken together, these restrictions implement the Liskov Substition Principle (LSP), which is a necessary condition for the safe use of object-oriented methods in critical software. See for example the DO-332 Object-Oriented Technology and Related Techniques supplement to DO-178C.
Sometimes, when declaring an overriding function, it is useful to compose a new postcondition by taking the inherited postcondition and adding some extra conditions. The token "..." may be used as one of the postconditions of an overriding function to represent the inherited postconditions.
User-defined operators are supported, with the following restrictions at present:
User-defined assigning operators and type conversion operators are not supported.
Class and function templates are supported, with the following restrictions at present:
For an example of verifying a class template with eCv++, see queue.cpp in the installed example files.
eCv Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.