main.tex 2.91 KB
Newer Older
1
%; whizzy section -pdf -initex "pdflatex -ini"
Julien Signoles's avatar
Julien Signoles committed
2
\documentclass[web]{frama-c-book}
3
4
5
6
7
8
9
10
11
12
13
14
\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}
15
%--\setboolean{ColorImplementationRq}{false}
16
17
18
19
20
21
22
23
24
25
26

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

27
\newcommand{\acslversion}{1.14\xspace}
28
\newcommand{\version}{\acslversion\xspace}
29
30
31
32
33
34
35
36
37
38
39

\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]
40
41
\mbox{\huge{Implementation in Frama-C plug-in E-ACSL}}\\[2mm]
\mbox{\huge{version \eacslversion{}}}}}}%
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
  {\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}
58
  \textcopyright 2011-2018 CEA LIST
59

60
61
  This work has been initially supported by the `Hi-Lite' FUI project (FUI AAP
  9).
62
63
64
65
66
67
68
69
70
71
72
\end{flushleft}
\end{titlepage}

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

\chapter*{Foreword}

Julien Signoles's avatar
Julien Signoles committed
73
74
75
76
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.
77
78
79
80
81
82

\section*{Acknowledgements}

We gratefully thank all the people who contributed to this document:
Patrick Baudin,
Bernard Botella,
Julien Signoles's avatar
Julien Signoles committed
83
Lo\"ic Correnson,
84
85
Pascal Cuoq,
Johannes Kanig,
Julien Signoles's avatar
Julien Signoles committed
86
Fonenantsoa Maurica,
Julien Signoles's avatar
Julien Signoles committed
87
David Mentr\'e,
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
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}