changes.tex 3.09 KB
Newer Older
1
2
3
4
5
\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.

6
\section*{E-ACSL 22.0 Titanium}
Julien Signoles's avatar
Julien Signoles committed
7

Julien Signoles's avatar
Julien Signoles committed
8
\begin{itemize}
9
\item Update every section with changes to \framac and \eacslgcc output
Julien Signoles's avatar
Julien Signoles committed
10
11
12
13
14
15
16
\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}

17
\begin{itemize}
18
19
\item \textbf{Runtime Monitor Behavior}: Document global variable
  \texttt{\_\_e\_acsl\_sound\_verdict} usable in \texttt{\_\_e\_acsl\_assert}.
20
\item New section \textbf{Partial Instrumentation}.
21
22
23
24
25
\item New section \textbf{Providing a White List of Functions}.
\end{itemize}

\section*{E-ACSL 18.0 Argon}

Julien Signoles's avatar
Julien Signoles committed
26
\begin{itemize}
27
\item \textbf{Introduction}: Improve a bit and reference new related papers.
28
\item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
Julien Signoles's avatar
Julien Signoles committed
29
  not yet robust.
30
\item \textbf{What the Plug-in Provides}: Highlight the importance of
Julien Signoles's avatar
Julien Signoles committed
31
  \textbf{-e-acsl-prepare}.
32
33
\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
  Monitoring Libraries'' by the new section ``Supported Systems''.
34
\item \textbf{Known Limitations}: Add limitation about monitoring of variables
35
  with incomplete types.
Julien Signoles's avatar
Julien Signoles committed
36
37
38
39
40
\end{itemize}

\section*{E-ACSL Chlorine-20180501}

\begin{itemize}
41
42
43
\item New section \textbf{Additional Verifications}.
\item Update every section with respect to the changes introduced since \eacsl
  Sulfur-20180101.
Julien Signoles's avatar
Julien Signoles committed
44
45
\end{itemize}

46
47
48
49
50
51
52
\section*{E-ACSL Sulfur-20180101}

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

\section*{E-ACSL Phosphorus-20170501}
53
54
55

\begin{itemize}
\item Removed chapter \textbf{Easy Instrumentation with E-ACSL}.
56
57
58
59
60
61
\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}.
62
\item \textbf{Known Limitations}: added section \textbf{Limitations of E-ACSL Monitoring Libraries}.
63
64
65
\item \textbf{Recursive Functions}: remove limitation about possible uses before
  being declared.
\item \textbf{Variadic Functions}: mention the \variadic plug-in.
66
67
68
\end{itemize}

\section*{E-ACSL 0.6}
Julien Signoles's avatar
Julien Signoles committed
69

Julien Signoles's avatar
Julien Signoles committed
70
71
72
73
74
75
\begin{itemize}
\item \textbf{Easy Instrumentation with E-ACSL}: new chapter.
\end{itemize}

\section*{E-ACSL 0.5}

76
\begin{itemize}
Julien Signoles's avatar
Julien Signoles committed
77
78
79
80
81
\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.
82
83
84
85
86
\item \textbf{Bibliography:} fix incorrect links.
\end{itemize}

\section*{E-ACSL 0.4}

Julien Signoles's avatar
Julien Signoles committed
87
\begin{itemize}
Julien Signoles's avatar
Julien Signoles committed
88
\item No change.
Julien Signoles's avatar
Julien Signoles committed
89
90
91
\end{itemize}

\section*{E-ACSL 0.3}
92
93
94
95
96
97
98
99
100
101
102
\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}