cpp-exceptions.tex

\section{Exceptions [C++]}
\label{sec:exceptions}
\index{exceptions,throws clause,\exception}

Exceptions are a C++ feature to enable structured alternate termination of a function, particularly when an error has occurred that is not locally recoverable. Although it can be challenging to implement exceptions efficiently, from the perspective of specification, exceptions are straightforward: they define alternate control paths, just like the various abrupt termination mechanisms of section \ref{sec:abrupt-clause}.

\begin{figure}[htp]
	\begin{cadre}
		\input{cpp-exceptionbehavior.bnf}
	\end{cadre}
	\caption{Grammar of contracts about exceptions}
	\label{fig:gram:throws-clause}
\end{figure}


The syntax additions related to exceptions are given in 
Figure~\ref{fig:gram:throws-clause}. Note the following points:
\begin{itemize}
\item A throws clause may be part of either a function contract or a statement contract.
%\item A throws clause may include a list of type names; these are the names of exception types for which the
%clause applies.
%\item The list of types may optionally be simply \ldots, meaning, as in C++, that the clause applies for any type.
%\item A throws clause with \ldots~for the list of type names is equivalent to the form with no type names at all.
\item The new term \lstinline|\exception| may be used within the clause's predicate; its value is a pointer to the exception object being thrown; its type is \lstinline|const void*|.
\item It is likely that to use the value of \lstinline|\exception|,
some additional information will be needed to determine the type and a
\lstinline|static\_cast| used to convert the \lstinline|void*| to a 
usable type.
%\item The new term \lstinline|\exception| may be used within the clause's predicate to refer to the exception object being thrown; its type is \lstinline|const T&|, where \lstinline|T| is the type of the thrown exception.
%\item If more than one type name is listed (or \ldots~for any type), the clauses's predicate must be syntactically and semantically valid for each possible type, with \lstinline|\exception| taking on each type in turn.
\item There is no implicit order to \textsl{throws} clauses.
\end{itemize}
The semantics of a \textsl{throws-clause} is that if the function or statement exits with an exception, then the predicate must be true in the post-state of the function or statement. This is similar to the \ensures and the other abrupt termination clauses: if the program construct terminates in the stated way, then the associated predicate must be true in the post-state (the pre-state for the \textsl{exits} clause).

Exception specifications are being deprecated in \lang. Consequently, \NAME does not specify or encourage tools to reason about \lang exception specifications, except for  uses of \textbf{noexcept} (cf. Section \ref{sec:attributes}).

\TODO{Add example}

\ifImpl{Status: throws clauses and the  \textbackslash exception keyword are parsed and checked by \fclang, but are not yet supported by \framac}