  VeriFast is a prototype tool based on separation logic for modular
verification of C and Java programs. We are in the process of adding support
for C++. In this report, we describe the features of C++ for which we added
support so far, as well as the proof obligations we generate for these
features. At this point, VeriFast has basic support for most object-oriented
programming features of C++: member functions, member function and operator
overloading, implicit and explicit conversions, constructors and initializer
lists, destructors, reference types, allocation and deallocation on the stack
or on the heap (using new and delete), inheritance (including multiple
inheritance but not virtual base classes), and virtual member functions and
overriding. To support specification of inheritance hierarchies, we added
support for instance predicates, which can be introduced in a base class and
overridden in derived classes. The main missing feature at this point is
support for C++ templates, which we plan to work on next.
