frama-c-book.cls

% --------------------------------------------------------------------------
% ---  LaTeX Class for Frama-C Books                                     ---
% --------------------------------------------------------------------------
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
\newif\ifusecc
\usecctrue
% --------------------------------------------------------------------------
% ---  Base Class management                                             ---
% --------------------------------------------------------------------------
\makeatletter
\RequirePackage{kvoptions}
\SetupKeyvalOptions{
family=framacbook,
prefix=framacbook@,
}
\RequirePackage{ifthen}
\DeclareVoidOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
\DeclareVoidOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
\DeclareStringOption[{type=CC,version=4.0,modifier=by-sa}]{license}
\DeclareStringOption[english]{lang}
\DeclareDefaultOption{\PassOptionsToClass{\CurrentOption}{report}}
\PassOptionsToClass{a4paper,11pt,twoside,openright}{report}

\ProcessKeyvalOptions*

\LoadClass{report}

\PassOptionsToPackage{\framacbook@lang}{babel}

\ifthenelse{\equal{\framacbook@license}{no}}{\useccfalse}{}
\ifusecc
  \PassOptionsToPackage{\framacbook@license}{doclicense}
\fi
\RequirePackage{babel}
\RequirePackage{fullpage}
\RequirePackage{lmodern}
\RequirePackage[T1]{fontenc}
\RequirePackage[utf8]{inputenc}
\RequirePackage{amssymb}
\RequirePackage[table]{xcolor}
\RequirePackage[pdftex]{graphicx}
\RequirePackage{ifthen}
\RequirePackage{xspace}
\RequirePackage{makeidx}
\RequirePackage[leftbars]{changebar}
\RequirePackage{fancyhdr}
\RequirePackage{titlesec}
\RequirePackage{upquote}
\RequirePackage[pdftex,pdfstartview=FitH]{hyperref}
\ifusecc\RequirePackage{doclicense}\else\fi
% --------------------------------------------------------------------------
% ---  Page Layout                                                       ---
% --------------------------------------------------------------------------
\setlength{\voffset}{-6mm}
\setlength{\headsep}{8mm}
\setlength{\footskip}{21mm}
\setlength{\textheight}{238mm}
\setlength{\topmargin}{0mm}
\setlength{\textwidth}{155mm}
\setlength{\oddsidemargin}{2mm}
\setlength{\evensidemargin}{-2mm}
\setlength{\changebarsep}{0.5cm}
\setlength{\headheight}{13.6pt}
\def\put@bg(#1,#2,#3)#4{\setlength\unitlength{1cm}%
  \begin{picture}(0,0)(#1,#2)
    \put(0,0){\includegraphics[width=#3cm]{#4}}
  \end{picture}}
\fancypagestyle{plain}{%
  \fancyfoot{}
  \fancyhead{}
  \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
  \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
  \fancyhead[CE]{\scriptsize\textsf{\leftmark}}
  \fancyhead[CO]{\scriptsize\textsf{\rightmark}}
  \fancyfoot[C]{\small\textsf{\thepage}}
  \renewcommand{\headrulewidth}{0pt}
  \renewcommand{\footrulewidth}{0pt}
}
\fancypagestyle{blank}{%
  \fancyfoot{}
  \fancyhead{}
  \fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
  \fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
}
%% Redefinition of cleardoublepage for empty page being blank
\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
\hbox{}
\thispagestyle{#1}
\newpage
\fi\fi}
\def\cleardoublepage{\cleardoublepagewith{blank}}
\pagestyle{plain}

% --------------------------------------------------------------------------
% ---  Cover Page                                                        ---
% --------------------------------------------------------------------------
\newcommand{\coverpage}[1]{%
\thispagestyle{empty}
\setlength\unitlength{1cm}
\begin{picture}(0,0)(3.27,26.75)
\put(0.58,0.70){\includegraphics[width=20.9cm]{frama-c-cover.pdf}}
\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
\end{picture}
}

% --------------------------------------------------------------------------
% ---  Title Page                                                        ---
% --------------------------------------------------------------------------
\renewenvironment{titlepage}%
{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
{\end{center}}
\renewcommand{\title}[2]{
\vspace{20mm}
{\Huge\bfseries #1}

\bigskip

{\LARGE #2}
\vspace{20mm}
}
\renewcommand{\author}[1]{
\vspace{20mm}

{#1}

\medskip
\ifusecc\doclicenseThis\else\fi
}

% \acknowledge{<flag image file>}{<text inside box>}
\newcommand{\acknowledge}[2]{
  \fbox{
    \begin{minipage}{0.97\textwidth}
      \begin{minipage}{1.2cm}
        \includegraphics[width=\linewidth]{#1}
      \end{minipage}
      \begin{minipage}{0.90\textwidth}
        This project has received funding from #2.
      \end{minipage}
    \end{minipage}
  }
}

\newcommand{\acknowledgeANR}{
  \acknowledge{anr-logo.png}{the French ANR projects
    CAT~(ANR-05-RNTL-00301) and U3CAT~(08-SEGI-021-01)
  }
}

\newcommand{\acknowledgeEU}{
  \acknowledge{eu-flag.jpg}{the
    European Union's Seventh Framework Programme (FP7/2007-2013)
    under grant agreement N$^\circ$\,317753 (\mbox{STANCE}).\\
    It has also received funding from the Horizon 2020 research
    and innovation programme, under grant agreements
    N$^\circ$\,731453~(\mbox{VESSEDIA}),
    N$^\circ$\,824231~(\mbox{DECODER}),
    N$^\circ$\,830892~(\mbox{SPARTA}),
    and N$^\circ$\,883242~(\mbox{ENSURESEC})
  }
}

% --------------------------------------------------------------------------
% ---  Sectionning                                                       ---
% --------------------------------------------------------------------------
\titleformat{\chapter}[display]{\Huge\raggedleft}%
{\huge\chaptertitlename\,\thechapter}{0.5em}{}
\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
[\vspace{-14pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}]
\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
[\vspace{-8pt}]

% --------------------------------------------------------------------------
% ---  Main Text Style                                                   ---
% --------------------------------------------------------------------------
%\raggedright
\setlength\parindent{0pt}
\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
\def\FramaC{\textsf{Frama-C}\xspace}
% --------------------------------------------------------------------------
% ---  Listings                                                          ---
% --------------------------------------------------------------------------
\RequirePackage{listings}

\lstdefinelanguage{ACSL}{%
  morekeywords={allocates,assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
    boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
    exit_behavior,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
    model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
    union,variant},
  keywordsprefix={\\},
  alsoletter={\\},
  morecomment=[l]{//}
}

\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
\definecolor{lstbg}{gray}{0.98}
\definecolor{lstfg}{gray}{0.10}
\definecolor{lstrule}{gray}{0.6}
\definecolor{lstnum}{gray}{0.4}
\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
\definecolor{lstfile}{gray}{0.85}
\newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\small\else\normalfont\ttfamily\mdseries\small\fi}
\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
\def\lp@keyword{}
\def\lp@special{\color{lstfg}}
\def\lp@comment{\normalfont\ttfamily\mdseries}
\def\lp@string{\color{lstfg}} \def\lp@ident{}
\def\lp@number{\rmfamily\tiny\color{lstnum}}
\lstdefinestyle{frama-c-style}{%
  columns=flexible,%
  basicstyle=\lp@inline,%
  identifierstyle=\lp@ident,%
  commentstyle=\lp@comment,%
  keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
  keywordstyle=[2]\lp@special,%
  stringstyle=\lp@string,%
  emphstyle=\lp@ident\underbar,%
  showstringspaces=false,%
  mathescape=true,%
  numberstyle=\lp@number,%
  xleftmargin=6ex,xrightmargin=2ex,%
  framexleftmargin=1ex,%
  frame=l,%
  framerule=1pt,%
  rulecolor=\color{lstrule},%
  backgroundcolor=\color{lstbg},%
  moredelim={*[s]{/*@}{*/}},%
  moredelim={*[l]{//@}},%
  morecomment={[il]{//NOPP-LINE}},% invisible comment until end of line
  morecomment={[is]{//NOPP-BEGIN}{NOPP-END\^^M}},% no space after NOPP-END
  mathescape=true,
  escapechar=`
% breaklines is broken when using a inline and background
%  breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
}

\lstdefinestyle{c}%
{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
\lstdefinestyle{c-basic}%
{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}


% --- C/ACSL Stuff ---------------------------------------------------------
% Make 'c' the default style
\lstset{style=c}

\newcommand{\listinginput}[3][1]%
{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}

\newcommand{\listinginputcaption}[4][1]%
{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,title=#3]{#4}}

\lstnewenvironment{listing}[2][1]%
{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}

\lstnewenvironment{listing-nonumber}%
{\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}

% --- Verbatim Stuff -------------------------------------------------------
\lstdefinelanguage{Shell}[]{csh}%
{escapechar=@
 identifierstyle=\lp@basic,
 mathescape=false,
 backgroundcolor=,
 literate={\\\$}{\$}1
}

\lstnewenvironment{shell}[1][]
{\lstset{language=Shell,basicstyle=\lp@basic,#1}}
{}

% ---- Stdout Stuff --------------------------------------------------------
\lstdefinelanguage{Logs}[]{csh}%
{identifierstyle=\lp@basic,backgroundcolor=}
\lstnewenvironment{logs}[1][]{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
\newcommand{\logsinput}[1]%
{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}

% --------------------------------------------------------------------------
% ---  Developer Code Stuff                                              ---
% --------------------------------------------------------------------------

\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}

% --- Style ----------------------------------------------------------------
\lstdefinestyle{framac-code-style}{%
basicstyle=\lp@inline,%
numberstyle=\lp@number,%
keywordstyle=[1]\sffamily\color{lstmodule},%
keywordstyle=[2]\sffamily\color{lstspecial},%
keywordstyle=[3]\sffamily\bfseries,%
identifierstyle=\rmfamily,%
stringstyle=\ttfamily\color{lstfg},%
commentstyle=\rmfamily\bfseries\color{lsttxt},%
}
\lstdefinestyle{framac-shell-style}{%
mathescape=false,%
basicstyle=\lp@basic,%
numberstyle=\lp@number,%
keywordstyle=\sffamily\bfseries,%
keywordstyle=[1]\sffamily\color{lstmodule},%
keywordstyle=[2]\sffamily\color{lstspecial},%
keywordstyle=[3]\sffamily\bfseries,%
identifierstyle=\ttfamily,%
stringstyle=\ttfamily\color{lstfg},%
commentstyle=\rmfamily\bfseries\color{lsttxt},%
literate={\\\$}{\$}1%
{€}{\textbackslash}1%
,%
}
% --- Configure ------------------------------------------------------------
\lstdefinelanguage{Configure}[]{csh}{%
style=framac-shell-style,%
morekeywords={fi},%
}
\lstnewenvironment{configurecode}[1][]%
{\lstset{language=Configure,#1}}{}
\newcommand{\configureinput}[1]{\lstinputlisting[language=Configure]{#1}}
% --- Makefile  ------------------------------------------------------------
\lstdefinelanguage{Makefile}[]{make}{%
style=framac-shell-style,%
morekeywords={include},%
}
\lstnewenvironment{makefilecode}[1][]%
{\lstset{language=Makefile,#1}}{}
\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
% --- C- for Developer  ----------------------------------------------------
\lstdefinestyle{framac-code}%
  {language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
\lstnewenvironment{ccode}[1][]%
{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
\newcommand{\cinput}[2][]%
{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1]{#2}}
\newcommand{\cinline}[1]%
{\lstinline[style=framac-code]{#1}}
% --- Ocaml ----------------------------------------------------------------
\lstdefinelanguage{Ocaml}[Objective]{Caml}{%
style=framac-code-style,%
deletekeywords={when,module,struct,sig,begin,end},%
morekeywords=[2]{failwith,raise,when},%
morekeywords=[3]{module,struct,sig,begin,end},%
literate=%
{~}{${\scriptstyle\thicksim}$}1%
{<}{$<$ }1%
{>}{$>$ }1%
{->}{$\rightarrow$ }1%
{<-}{$\leftarrow$ }1%
{:=}{$\leftarrow$ }1%
{<=}{$\leq$ }1%
{>=}{$\geq$ }1%
{==}{$\equiv$ }1%
{!=}{$\not\equiv$ }1%
{<>}{$\neq$ }1%
{'a}{$\alpha$ }1%
{'b}{$\beta$ }1%
{'c}{$\gamma$ }1%
{µ}{`{}}1%
{€}{\textbackslash}1%
{à}{{\`a}}1%
{é}{{\'e}}1%
}
\lstdefinestyle{ocaml-basic}{
  language=Ocaml,
  basicstyle=\lp@basic
}

\lstdefinelanguage{Dune}{%
literate=%
{à}{{\`a}}1%
{é}{{\'e}}1%
,
  style=framac-code-style,%
  morekeywords={
    dune, flags, generate_opam_files, lang, libraries, name, optional, package,
    plugin, public_name, site, using
  },%
  morekeywords=[2]{
    :standard
  },
  morecomment=[l]{;},
}
\lstdefinestyle{dune-basic}{%
  language=Dune,%
  style=framac-code-style,%
  basicstyle=\lp@inline,%
}

\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
\newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}}
\lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{}
% --------------------------------------------------------------------------
\lstdefinelanguage{Why}{%
  morekeywords={
    type, logic, axiom, predicate, goal,
    forall, let, in,
  },
  morecomment=[s]{(*}{*)},
  alsoletter={_},
  literate=%
  {->}{$\Rightarrow$}1%
  {forall}{$\forall$}1%
  {not}{$\neg$}1%
  {<>}{$\neq$}1%
  {...}{$\dots$}1%
  %{_}{\_}1%
  %{_}{{\rule[0pt]{1ex}{.2pt}}}1%
  }

\lstdefinestyle{why-style}{%
language=Why,%
style=framac-code-style,%
basicstyle=\lp@inline,%
}

\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
\newcommand{\whyinput}[1]%
{\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}}
\newcommand{\whyinline}[1]%
{\lstinline[style=why-style]{#1}}
\makeatother
% --------------------------------------------------------------------------
% ---  End.                                                              ---
% --------------------------------------------------------------------------