changes.tex

\chapter{Changes}\label{chap:changes}

This chapter summarizes the changes in this documentation between each \eacsl
release. First we list changes of the last release.

\section*{E-ACSL 22.0 Titanium}

\begin{itemize}
\item Update every section with changes to \framac and \eacslgcc output
\item \textbf{Simple Example}: Remove option \texttt{-e-acsl-check}
\item \textbf{Combining E-ACSL with Other PLug-ins}: \texttt{-e-acsl-prepare} is
  no more necessary.
\end{itemize}

\section*{E-ACSL 19.0 Potassium}

\begin{itemize}
\item \textbf{Runtime Monitor Behavior}: Document global variable
  \texttt{\_\_e\_acsl\_sound\_verdict} usable in \texttt{\_\_e\_acsl\_assert}.
\item New section \textbf{Partial Instrumentation}.
\item New section \textbf{Providing a White List of Functions}.
\end{itemize}

\section*{E-ACSL 18.0 Argon}

\begin{itemize}
\item \textbf{Introduction}: Improve a bit and reference new related papers.
\item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
  not yet robust.
\item \textbf{What the Plug-in Provides}: Highlight the importance of
  \textbf{-e-acsl-prepare}.
\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
  Monitoring Libraries'' by the new section ``Supported Systems''.
\item \textbf{Known Limitations}: Add limitation about monitoring of variables
  with incomplete types.
\end{itemize}

\section*{E-ACSL Chlorine-20180501}

\begin{itemize}
\item New section \textbf{Additional Verifications}.
\item Update every section with respect to the changes introduced since \eacsl
  Sulfur-20180101.
\end{itemize}

\section*{E-ACSL Sulfur-20180101}

\begin{itemize}
\item no changes
\end{itemize}

\section*{E-ACSL Phosphorus-20170501}

\begin{itemize}
\item Removed chapter \textbf{Easy Instrumentation with E-ACSL}.
\item \textbf{What the Plug-in Provides}: added section \textbf{E-ACSL Wrapper
  Script}.
\item \textbf{What the Plug-in Provides}: added description of \eacsl runtime
  libraries.
\item \textbf{Known Limitations}: added section \textbf{Requirements to Input
  Programs}.
\item \textbf{Known Limitations}: added section \textbf{Limitations of E-ACSL Monitoring Libraries}.
\item \textbf{Recursive Functions}: remove limitation about possible uses before
  being declared.
\item \textbf{Variadic Functions}: mention the \variadic plug-in.
\end{itemize}

\section*{E-ACSL 0.6}

\begin{itemize}
\item \textbf{Easy Instrumentation with E-ACSL}: new chapter.
\end{itemize}

\section*{E-ACSL 0.5}

\begin{itemize}
\item \textbf{Libc}: new section.
\item \textbf{Architecture Dependent Annotations}: add a remark about \gcc's
  machdep.
\item Use \texttt{-then-last} whenever possible.
\item Update output wrt \framac Sodium changes.
\item \textbf{Bibliography:} fix incorrect links.
\end{itemize}

\section*{E-ACSL 0.4}

\begin{itemize}
\item No change.
\end{itemize}

\section*{E-ACSL 0.3}
\begin{itemize}
\item \textbf{Introduction:} reference the \eacsl tutorial.
\item \textbf{Memory-related Annotations:} document the
  \lstinline|E_ACSL_MACHDEP| macro.
\end{itemize}

\section*{E-ACSL 0.2}

\begin{itemize}
\item First release of this manual.
\end{itemize}