%; whizzy section -pdf -initex "pdflatex -ini"
\documentclass[web]{frama-c-book}
\usepackage{hevea}
\usepackage{ifthen}

\input{./macros_modern}
\input{eacslversion.tex}
%Do not touch the following line. It is used in a Makefile hack to
%produce the ACSL documents for the ACSL working group.
%--\setboolean{PrintRemarks}{false}

%Do not touch the following line. It is used in a Makefile hack to
%produce the ACSL document shipped with the Frama-C distribution.
%--\setboolean{PrintImplementationRq}{false}
%--\setboolean{ColorImplementationRq}{false}

\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{color}
\usepackage{xspace}
\usepackage{makeidx}
\usepackage[normalem]{ulem}
\usepackage[leftbars]{changebar}
\usepackage{alltt}
\makeindex

\newcommand{\acslversion}{1.14\xspace}
\newcommand{\version}{\acslversion\xspace}

\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}

\begin{document}
\sloppy
\hbadness=10000

\ifthenelse{\boolean{PrintImplementationRq}}%
  {\coverpage{\vbox{\mbox{E-ACSL Version \version}\\[5mm]
\mbox{\huge{Implementation in Frama-C plug-in E-ACSL}}\\[2mm]
\mbox{\huge{version \eacslversion{}}}}}}%
  {\coverpage{\vbox{\mbox{E-ACSL}\\[2mm]\vbox{\mbox{\huge{Executable ANSI/ISO C
          Specification Language}}}\\[2mm]
        \mbox{Version \version}}}}

\begin{titlepage}
\includegraphics[height=14mm]{cealistlogo.jpg}
\vfill
\title{E-ACSL\\[5mm]\huge{Executable ANSI/ISO C Specification Language}}%
{Version \version{}\ifthenelse{\boolean{PrintImplementationRq}}%
{~--~Frama-C plug-in E-ACSL version \eacslversion}{}}

\author{Julien Signoles}

CEA LIST, Software Reliability Laboratory\\
\vfill
\begin{flushleft}
  \textcopyright 2011-2018 CEA LIST

  This work has been initially supported by the `Hi-Lite' FUI project (FUI AAP
  9).
\end{flushleft}
\end{titlepage}

%%Contents should open on right
\cleardoublepage
\phantomsection
\label{chap:contents}
\tableofcontents

\chapter*{Foreword}

This document describes version \version of the \eacsl specification
language. It is based on the \acsl specification language~\cite{acsl}. Features
of both languages may still evolve in the future, even if we do our best to
preserve backward compatibility.

\section*{Acknowledgements}

We gratefully thank all the people who contributed to this document:
Patrick Baudin,
Bernard Botella,
Lo\"ic Correnson,
Pascal Cuoq,
Johannes Kanig,
Fonenantsoa Maurica,
David Mentr\'e,
Benjamin Monate,
Yannick Moy and
Virgile Prevosto.

\include{intro_modern}

\include{speclang_modern}

\include{libraries_modern}

\include{concl_modern}

\appendix

\chapter{Appendices}
\label{chap:appendix}

\include{changes_modern}

\cleardoublepage
\addcontentsline{toc}{chapter}{\bibname}
\bibliographystyle{plain}
\bibliography{./biblio}

\cleardoublepage
\addcontentsline{toc}{chapter}{\listfigurename}
\listoffigures

\cleardoublepage
\addcontentsline{toc}{chapter}{\indexname}
\printindex

\end{document}