user-changes.tex

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

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

\section*{21.0 (Scandium)}

\begin{itemize}
\item \textbf{Preparing the Sources:} added option
  \texttt{-cpp-extra-args-per-file}.
\item \textbf{Customizing Analyzers:} added options
  \texttt{-warn-invalid-pointer} and \texttt{-warn-pointer-downcast}
\end{itemize}

\section*{20.0 (Calcium)}

\begin{itemize}
\item \textbf{Normalizing the Source Code:} added options
  \texttt{-keep-unused-types} and its opposite,
  \texttt{-remove-unused-types}.
\end{itemize}

\section*{18.0 (Argon)}

\begin{itemize}
\item \textbf{Feedback Options:} change options governing status of warning categories
\item \textbf{Normalizing the Source Code:} added category \texttt{@inline} to
option \texttt{-inline-calls}, and added option \texttt{-remove-inlined}.
\item \textbf{Customizing Analyzers:} added options
  \texttt{-warn-left-shift-negative}, \\
  \texttt{-warn-right-shift-negative} and \\
  \texttt{-warn-invalid-bool}.
\end{itemize}

\section*{Chlorine-20180501}

\begin{itemize}
\item \textbf{Normalizing the Source Code:} added option \texttt{-inline-calls}.
\item \textbf{Preparing the Sources:} documentation of macros that can be
  defined to customize the standard C library.
\item \textbf{Preparing the Sources:} deprecated option
  \texttt{-implicit-function-declaration} (superseded by
  warning categories; equivalent to\\
  \texttt{-kernel-warn-\{key,abort,feedback\} typing:implicit-function-declaration}).
\item \textbf{Setting Up Plug-ins:} remove obsolete references
 to static plug-ins and \texttt{--with-all-static} configure option.
\item \textbf{Feedback Options:} introduction of warning categories and statuses.
\item \textbf{Customizing Analyzers:} added option \texttt{-warn-special-float}.
\item \textbf{Preparing the Sources:} added option
  \texttt{-json-compilation-database}.
\item \textbf{Reports:} new chapter documenting reporting facilities.
\item \textbf{Variadic Plug-in:} new chapter documenting the Variadic plug-in.
\end{itemize}

\section*{Sulfur-20171101}

\begin{itemize}
\item \textbf{Preparing the Sources:} removed option
  \texttt{-force-rl-arg-eval}.
\item \textbf{Normalizing the Source Code:} added section about compiler
  and language extensions (Section~\ref{sec:extensions}).
\item \textbf{Normalizing the Source Code:} removed option
  \texttt{-custom-annot-char}.
\end{itemize}

\section*{Phosphorus-20170501}

\begin{itemize}
\item \textbf{Getting Started:} \tool{Zarith} package is now mandatory.
\item \textbf{Setting Up Plug-ins:} added option \texttt{-autoload-plugins}.
\item \textbf{Preparing the Sources:} renamed option \texttt{-cpp-gnu-like}
  to \texttt{-cpp-frama-c-compliant}.
\item \textbf{Getting Started:} document new bash completion script.
\item \textbf{Getting Started:} added option \texttt{-print-libc}.
\end{itemize}

\section*{Silicon-20161101}

\begin{itemize}
\item \textbf{Getting Started:} OCaml version greater or equal than 4.05.0 is required
\item \textbf{Normalizing the Source Code:} New option \texttt{-c11}
\end{itemize}

\section*{Aluminium-20160501}

\begin{itemize}
\item \textbf{Getting Started:} document new option \texttt{-then-replace}.
\item \textbf{Getting Started:} document new option
\texttt{-set-project-as-default}.
\item \textbf{Project:} document new option \texttt{-remove-projects}.
\item \textbf{Getting Started:} document new option
  \texttt{-<plug-in shortname>-log}.
\item \textbf{Normalizing the Source Code:} document new options
  \texttt{-asm-contracts} and\\ \texttt{-asm-contracts-auto-validate}
\item \textbf{Graphical User Interface:} Option \texttt{-collect-messages} is
  active by default, and cannot be deactivated.
\end{itemize}

\section*{Magnesium-20151001}
\begin{itemize}
\item \textbf{Getting Started:} support is not guaranteed for OCaml versions
below 4.x.
\item \textbf{Getting Started:} the recommended installation method now consists
in using the Frama-C OPAM package.
\item \textbf{Normalizing the Source Code:} option \texttt{-pp-annot} is now
active by default.
\item \textbf{Normalizing the Source Code:} added section about macros
predefined by \FramaC (Section~\ref{sec:predefined-macros}).
\item \textbf{Normalizing the Source Code:} document new option 
  \texttt{-custom-annot-char} (Section~\ref{sec:normalize})
\item \textbf{Normalizing the Source Code:} document handling of 
  new file suffix \texttt{.ci} (Section~\ref{sec:preprocessing})
\item \textbf{Preparing the Sources:} option \texttt{-warn-undefined-callee}
  changed to \\ \texttt{-implicit-function-declaration warn}.
\item \textbf{Setting Up Plug-ins:} removed option \texttt{-dynlink}.
\end{itemize}

\section*{Sodium-20150201}
\begin{itemize}
\item \textbf{Normalizing the Source Code:} new options
  \texttt{-initialized-padding-locals} and \texttt{-simplify-trivial-loops}.
\item \textbf{Pre-processing the Source Files:} new options
  \texttt{-cpp-gnu-like} and \texttt{-frama-c-stdlib}.
\item \textbf{Customizing Analyzers:} new options
  \texttt{-add-symbolic-path} and \texttt{-permissive}.
\item \textbf{Getting Started:} document options containing several values
  (\emph{aka} set and map).
\item \textbf{Getting Started:} improve documentation of options.
\item \textbf{Getting Started:} document new option \texttt{-then-last}.
\item \textbf{Getting Started:} document new option \texttt{-tty}.
\end{itemize}

\section*{Neon-20140*01}
\begin{itemize}
\item \textbf{Getting Started:} fixes list of requirements 
  for compiling \FramaC.
\item \textbf{Preparing the Sources:} new option \texttt{-aggressive-merging}
\item \textbf{General Kernel Services:} change the default name of the journal.
\item \textbf{Getting Started:} 
  new options \texttt{-config} and \texttt{-<plug-in shortname>-config}, as
  well as new environment variable \texttt{FRAMAC\_CONFIG}.
\item \textbf{Getting Started:} 
  new options \texttt{-session} and \texttt{-<plug-in shortname>-session}, as
  well as new environment variable \texttt{FRAMAC\_SESSION}.
\item \textbf{Getting Started:} document option \texttt{-unicode}.
\item \textbf{General Kernel Services:} clarify when saving is done.
\end{itemize}

\section*{Fluorine-20130*01}
\begin{itemize}
\item \textbf{Getting Started:} update installation requirements.
\item \textbf{Customizing Analyzers:} document the following new options:
  \begin{itemize}
  \item \texttt{-warn-signed-overflow},
  \item \texttt{-warn-unsigned-overflow},
  \item \texttt{-warn-signed-downcast}, and
  \item \texttt{-warn-unsigned-downcast}.
  \end{itemize}
\item \textbf{Preparing the Sources:} document new option \texttt{-enums}
\end{itemize}

\section*{Oxygen-20120901}

\begin{itemize}
\item \textbf{Analysis Option:} better documentation of 
\texttt{-unspecified-access}
\item \textbf{Preparing the Sources:} better documentation of \texttt{-pp-annot}
\item \textbf{Preparing the Sources:} pragma \texttt{UNROLL\_LOOP} is
deprecated in favor of \texttt{UNROLL}
\item \textbf{Preparing the Sources:} document new normalization options
  \texttt{-warn-decimal-float}, \texttt{-warn-undeclared-callee} and
  \texttt{-keep-unused-specified-functions}
\item \textbf{General Kernel Services:} document special cases of saving and
  journalisation.
\item \textbf{Getting Started:} optional \tool{Zarith} package.
\item \textbf{Getting Started:} new option \texttt{-<plug-in shortname>-share}.
\end{itemize}

\section*{Nitrogen-20111001}

\begin{itemize}
\item \textbf{Overview:} report on Frama-C' usage as an educational tool.
\item \textbf{Getting Started:} exit status 127 is now 125 (127 and 126 are
reserved by POSIX).
\item \textbf{Getting Started:} update options for controlling display of
  floating-point numbers
\item \textbf{Preparing the sources:} document generation of \texttt{assigns}
  clause for function prototypes without body and proper specification
\item \textbf{Property Statuses:} new chapter to document property statuses.
\item \textbf{GUI:} document new interface elements.
\end{itemize}

\section*{Carbon-20110201}

\begin{itemize}
\item \textbf{Getting Started:} exit status 5 is now 127;
new exit status 5 and 6.
\item \textbf{GUI:} document new options \texttt{-collect-messages}.
\end{itemize}

\section*{Carbon-20101201}

\begin{itemize}
\item \textbf{Getting Started:} document new options \texttt{-then} and
  \texttt{-then-on}.
\item \textbf{Getting Started:} option \texttt{-obfuscate} is no more a kernel
  option since the obfuscator is now a plug-in.
\end{itemize}

\section*{Boron-20100401}

\begin{itemize}
\item \textbf{Preparing the Sources:} document usage of the C standard library
  delivered with \FramaC
\item \textbf{Graphical User Interface:} simplified and updated according to
  the new implementation
\item \textbf{Getting Started:} document environment variables altogether
\item \textbf{Getting Started:} document all the ways to getting help
\item \textbf{Getting Started:} \tool{OcamlGraph} 1.4 instead 1.3 will be used
  if previously installed
\item \textbf{Getting Started:} \tool{GtkSourceView} 2.x instead of 1.x is now
  required for building the GUI
\item \textbf{Getting Started:} documentation of the option
  \texttt{-float-digits}
\item \textbf{Preparing the Sources:} documentation of the option
  \texttt{-continue-annot-error}
\item \textbf{Using plug-ins:} new option \texttt{-dynlink}
\item \textbf{Journalisation:} a journal is generated only whenever \FramaC
  crashes on the GUI
\item \textbf{Configure:} new option \texttt{-{}-with-no-plugin}
\item \textbf{Configure:} option \texttt{-{}-with-all-static} set by default
  when native dynamic loading is not available
\end{itemize}

\section*{Beryllium-20090902}

\begin{itemize}
\item First public release
\end{itemize}

%% Local Variables:
%% compile-command: "make"
%% ispell-local-dictionary: "english"
%% TeX-master: "userman.tex"
%% End: