.. _features: ################# Language Support ################# The |project| program logic is aimed to be a formalization of pragmatic C++. Its feature set is guided by the requirements of low-level program verification and also some pragmatic considerations. Limitations of |project| ========================= |project| does not cover the full feature set of C++. Some features that are explicitly **not supported** are: * The |project| program logic *assumes* that the abstract syntax tree is well-typed and uses this assumption to avoid performing type checking within the semantics. If you are using `cpp2v` to generate the AST, then Clang will ensure that the syntax tree is well typed. * |project| is based on the Clang front-end IR. We believe that this is a reasonable proxy for source-level C++. * Exceptions. In addition to not supporting :cpp:`throw` and :cpp:`try`, |project| additionally assumes that function calls do not throw exceptions. * :cpp:`virtual` inheritance. * Floating point values and operations * Labeled statements and :cpp:`goto` are not supported. * :cpp:`switch` statements have restricted semantics when mixed with control flow. * Bitfields * :cpp:`[packed]` data structures. While not supported right now, some features are on our road map. * Translation unit initialization (i.e. initialization of globals) * :cpp:`template` code can only be reasoned about *after* instantiating it to specific arguments. * Weak memory accesses. |project| currently requires that all atomic accesses are sequentially consistent [#weak-mem]_. * Member pointers (and associated operators, i.e. :cpp:`.*` and :cpp:`->*`) * Member functions, constructors, and destructors are modeled by translating them to functions. This is unsound but requires :cpp:`reinterpret_cast` to exploit. * The semantics currently ignores :cpp:`volatile` qualifiers. * We rely on the semantics of defaulted functions (e.g. default constructors, assignment operators, etc) generated by Clang. If your compiler generates different code (but still semantically correct code), this may invalidate your proof. We recommend using Clang *with exactly the same build parameters as those used in your build* for the best compatibility. * `Transparent replacement `_. * Verification of variadic functions (e.g. :cpp:`printf`) is not supported, but calling variadic functions is supported. Deviations from the Standard ============================= In certain instances, |project|'s semantics deviates from the C++ standard. * |project|'s semantics do not currently permit "pointer zapping". See :ref:`no-pointer-zapping`. * |project| uses `Tnum sz sgn` to represent all integer types rather than the standard types :cpp:`char`, :cpp:`short`, :cpp:`int`, :cpp:`long`, :cpp:`long long`. Known Issues ============= There are several known issues with the current |project| semantics; we are working to support these. * |project| semantics does not currently support flexible array members. These are not officially supported by the standard but are frequently used in C++ programs. Extensions to the Standard =========================== |project| also extends the C++ standard in limited ways to make low-level program verification possible. For example, inter-operation with assembly (see :ref:`machine-interop`), sharing data across address spaces, etc. We believe that our extensions are conservative and characterize the way that low-level programmers rely on compilers to work. .. [#weak-mem] We plan to support weak memory C++ in the future based on other work in Iris.