Commit bd483665 authored by Julien Signoles's avatar Julien Signoles

Merge branch 'feature/basile/eacsl-manual-updates' into 'stable/titanium'

[eacsl] Update E-ACSL manuals for Titanium release

See merge request frama-c/frama-c!2948
parents 10445eae 71073bba
FRAMAC_DOC_ROOT_DIR?=..
FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf
frama-c-book.cls: ../frama-c-book.cls frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls
@rm -f $@ @rm -f $@
@cp $< . @cp $< .
@chmod a-w $@ @chmod a-w $@
@echo "import $<" @echo "import $<"
frama-c-cover.pdf: ../frama-c-cover.pdf frama-c-cover.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-cover.pdf
@rm -f $@ @rm -f $@
@cp $< . @cp $< .
@chmod a-w $@ @chmod a-w $@
@echo "import $<" @echo "import $<"
frama-c-right.pdf: ../frama-c-right.pdf frama-c-right.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-right.pdf
@rm -f $@ @rm -f $@
@cp $< . @cp $< .
@chmod a-w $@ @chmod a-w $@
@echo "import $<" @echo "import $<"
frama-c-left.pdf: ../frama-c-left.pdf frama-c-left.pdf: $(FRAMAC_DOC_ROOT_DIR)/frama-c-left.pdf
@rm -f $@ @rm -f $@
@cp $< . @cp $< .
@chmod a-w $@ @chmod a-w $@
......
...@@ -355,8 +355,6 @@ EACSL_MANPAGES := \ ...@@ -355,8 +355,6 @@ EACSL_MANPAGES := \
EACSL_CONTRIB_FILES = \ EACSL_CONTRIB_FILES = \
$(EACSL_DLMALLOC_REL_DIR)/dlmalloc.c $(EACSL_DLMALLOC_REL_DIR)/dlmalloc.c
EACSL_MANUAL_FILES = doc/manuals/*.pdf
EACSL_DOC_FILES = \ EACSL_DOC_FILES = \
doc/doxygen/doxygen.cfg.in \ doc/doxygen/doxygen.cfg.in \
doc/Changelog \ doc/Changelog \
...@@ -479,8 +477,6 @@ include $(FRAMAC_SHARE)/Makefile.dynamic ...@@ -479,8 +477,6 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
# Install # # Install #
########### ###########
EACSL_INSTALL_MANUAL_FILES=$(wildcard $(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_MANUAL_FILES)))
EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS)) EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS))
EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES)) EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES))
...@@ -491,13 +487,6 @@ install:: ...@@ -491,13 +487,6 @@ install::
$(MKDIR) $(FRAMAC_DATADIR)/$$dir && \ $(MKDIR) $(FRAMAC_DATADIR)/$$dir && \
$(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \ $(CP) $(E_ACSL_DIR)/share/$$dir/*.[ch] $(FRAMAC_DATADIR)/$$dir ; \
done done
# manuals are not present in standard distribution.
# Don't fail because of that.
ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","")
$(PRINT_INSTALL) E-ACSL manuals
$(MKDIR) $(FRAMAC_DATADIR)/manuals
$(CP) $(EACSL_INSTALL_MANUAL_FILES) $(FRAMAC_DATADIR)/manuals;
endif
$(PRINT_INSTALL) E-ACSL libraries $(PRINT_INSTALL) E-ACSL libraries
$(MKDIR) $(LIBDIR) $(MKDIR) $(LIBDIR)
$(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR) $(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR)
...@@ -516,8 +505,6 @@ EACSL_INSTALLED_MANPAGES=$(addprefix $(MANDIR)/man1/,$(notdir $(EACSL_MANPAGES)) ...@@ -516,8 +505,6 @@ EACSL_INSTALLED_MANPAGES=$(addprefix $(MANDIR)/man1/,$(notdir $(EACSL_MANPAGES))
uninstall:: uninstall::
$(PRINT_RM) E-ACSL share files $(PRINT_RM) E-ACSL share files
$(RM) -r $(FRAMAC_DATADIR)/e-acsl $(RM) -r $(FRAMAC_DATADIR)/e-acsl
$(PRINT_RM) E-ACSL manuals
$(RM) $(FRAMAC_DATADIR)/manuals/*.pdf
$(PRINT_RM) E-ACSL libraries $(PRINT_RM) E-ACSL libraries
$(RM) $(LIBDIR)/libeacsl-*.a $(RM) $(LIBDIR)/libeacsl-*.a
$(PRINT_RM) E-ACSL scripts $(PRINT_RM) E-ACSL scripts
......
...@@ -30,7 +30,7 @@ Plugin E-ACSL 22.0 (Titanium) ...@@ -30,7 +30,7 @@ Plugin E-ACSL 22.0 (Titanium)
############################# #############################
-* E-ACSL [2020-11-16] Fix soundness bug when checking -* E-ACSL [2020-11-16] Fix soundness bug when checking
initialization of a chunk of heap memory block. initialization of a chunk of heap memory block.
- E-ACSL [2020-10-14] Add Support for Variadic generated functions in - E-ACSL [2020-10-14] Add Support for Variadic generated functions in
the AST (frama-c/e-acsl#128). the AST (frama-c/e-acsl#128).
- E-ACSL [2020-10-06] Add support for the `\separated` predicate. - E-ACSL [2020-10-06] Add support for the `\separated` predicate.
......
frama-c-book.cls
frama-c-cover.pdf
frama-c-left.pdf
frama-c-right.pdf
e-acsl.pdf e-acsl.pdf
e-acsl-implementation.pdf e-acsl-implementation.pdf
eacslversion.tex eacslversion.tex
...@@ -27,13 +27,13 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \ ...@@ -27,13 +27,13 @@ DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
e-acsl: e-acsl-implementation.pdf e-acsl.pdf e-acsl: e-acsl-implementation.pdf e-acsl.pdf
all: e-acsl all: e-acsl
e-acsl-implementation.pdf: $(DEPS_MODERN) e-acsl-implementation.pdf: $(DEPS_MODERN) $(FRAMAC_MODERN)
e-acsl-implementation.tex: $(MAIN).tex Makefile e-acsl-implementation.tex: $(MAIN).tex Makefile
rm -f $@ rm -f $@
sed -e '/PrintRemarks/s/%--//' $^ > $@ sed -e '/PrintRemarks/s/%--//' $^ > $@
chmod a-w $@ chmod a-w $@
e-acsl.pdf: $(DEPS_MODERN) e-acsl.pdf: $(DEPS_MODERN) $(FRAMAC_MODERN)
e-acsl.tex: e-acsl-implementation.tex Makefile e-acsl.tex: e-acsl-implementation.tex Makefile
rm -f $@ rm -f $@
sed -e '/PrintImplementationRq/s/%--//' \ sed -e '/PrintImplementationRq/s/%--//' \
...@@ -43,13 +43,6 @@ e-acsl.tex: e-acsl-implementation.tex Makefile ...@@ -43,13 +43,6 @@ e-acsl.tex: e-acsl-implementation.tex Makefile
$(MAIN).pdf: $(DEPS_MODERN) $(MAIN).pdf: $(DEPS_MODERN)
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
install: e-acsl-implementation.pdf e-acsl.pdf
mkdir -p $(EACSL_DIR)/doc/manuals
cp -f $^ $(EACSL_DIR)/doc/manuals
include $(EACSL_DIR)/doc/support/MakeLaTeXModern
.PHONY: clean .PHONY: clean
clean: clean:
rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \ rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
C-compound-statement ::= "{" declaration* statement* assertion+ "}" C-compound-statement ::= "{" declaration* statement* assertion+ "}"
\ \
C-statement ::= assertion statement \ C-statement ::= assertion statement \
assertion-kind ::= "assert" | "check" \ assertion-kind ::= "assert" | clause-kind \
assertion ::= "/*@" assertion-kind pred ";" "*/" ; assertion ::= "/*@" assertion-kind pred ";" "*/" ;
| { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ; | { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
\end{syntax} \end{syntax}
...@@ -2,82 +2,82 @@ ...@@ -2,82 +2,82 @@
@STRING{LNCS = {Lecture Notes in Computer Science}} @STRING{LNCS = {Lecture Notes in Computer Science}}
@INPROCEEDINGS{jml, @inproceedings{jml,
author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll
and Clyde Ruby and Bart Jacobs}, and Clyde Ruby and Bart Jacobs},
title = {{JML}: notations and tools supporting detailed design in {Java}}, title = {{JML}: notations and tools supporting detailed design in {Java}},
booktitle = {{OOPSLA} 2000 Companion, Minneapolis, Minnesota}, booktitle = {{OOPSLA} 2000 Companion, Minneapolis, Minnesota},
pages = {105--106}, pages = {105--106},
year = 2000 year = 2000,
} }
@INPROCEEDINGS{chalin07, @inproceedings{chalin07,
author = {Patrice Chalin}, author = {Patrice Chalin},
title = {A Sound Assertion Semantics for the Dependable Systems Evolution title = {A Sound Assertion Semantics for the Dependable Systems Evolution
Verifying Compiler}, Verifying Compiler},
booktitle = {Proceedings of the International Conference on Software booktitle = {Proceedings of the International Conference on Software
Engineering (ICSE'07)}, Engineering (ICSE'07)},
pages = {23-33}, pages = {23-33},
year = 2007, year = 2007,
address = {Los Alamitos, CA, USA}, address = {Los Alamitos, CA, USA},
publisher = {IEEE Computer Society} publisher = {IEEE Computer Society},
} }
@INPROCEEDINGS{chalin05, @inproceedings{chalin05,
author = {Patrice Chalin}, author = {Patrice Chalin},
title = {Reassessing {JML}'s Logical Foundation}, title = {Reassessing {JML}'s Logical Foundation},
booktitle = {Proceedings of the 7th Workshop on Formal Techniques for booktitle = {Proceedings of the 7th Workshop on Formal Techniques for
Java-like Programs (FTfJP'05)}, Java-like Programs (FTfJP'05)},
year = 2005, year = 2005,
address = {Glasgow, Scotland}, address = {Glasgow, Scotland},
month = JUL month = JUL,
} }
@manual{acsl, @manual{acsl,
title = {{ACSL, ANSI/ISO C Specification Language}}, title = {{ACSL, ANSI/ISO C Specification Language}},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto}, Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
note = {Vesion 1.12. \url{http://frama-c.com/acsl.html}}, note = {\url{https://frama-c.com/html/acsl.html}},
} }
@manual{acslimplem, @manual{acslimplem,
title = {{ACSL version 1.12, Implementation in Silicon-20161101}}, title = {{ACSL, Implementation in Frama-C}},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto}, Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
note = {\url{http://frama-c.com/acsl.html}}, note = {\url{https://frama-c.com/download/frama-c-acsl-implementation.pdf}},
} }
@manual{framac, @manual{framac,
title = {Frama-C User Manual}, title = {Frama-C User Manual},
author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
André Maroneze and André Maroneze and
Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski}, Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski},
note = {\url{http://frama-c.com}}, note = {\url{https://frama-c.com/download/frama-c-user-manual.pdf}},
} }
@manual{eacsl-plugin, @manual{eacsl-plugin,
title = {Frama-C's E-ACSL Plug-in}, title = {Frama-C's E-ACSL Plug-in},
author = {Julien Signoles and Kostyantyn Vorobyov}, author = {Julien Signoles and Kostyantyn Vorobyov},
note = {\url{http://frama-c.com/eacsl.html}}, note = {\url{https://frama-c.com/fc-plugins/e-acsl.html}},
} }
@manual{value, @manual{value,
title = {Frama-C's value analysis plug-in}, title = {Frama-C's Evolved Value Analysis analysis plug-in},
author = {Pascal Cuoq and Boris Yakobowski and Matthieu Lemerre and author = {Pascal Cuoq and Boris Yakobowski and Matthieu Lemerre and
André Maroneze and Valentin Perelle and Virgile Prevosto}, André Maroneze and Valentin Perelle and Virgile Prevosto},
note = {\url{http://frama-c.com/value.html}}, note = {\url{https://frama-c.com/fc-plugins/eva.html}},
} }
@BOOK{KR88, @book{KR88,
author = {Brian Kernighan and Dennis Ritchie}, author = {Brian Kernighan and Dennis Ritchie},
title = {The C Programming Language (2nd Ed.)}, title = {The C Programming Language (2nd Ed.)},
publisher = {Prentice-Hall}, publisher = {Prentice-Hall},
year = 1988 year = 1988,
} }
@MANUAL{standardc99, @manual{standardc99,
title = {The {ANSI C} standard ({C99})}, title = {The {ANSI C} standard ({C99})},
organization = {International Organization for Standardization ({ISO})}, organization = {International Organization for Standardization ({ISO})},
key = {C99}, key = {C99},
note = {\url{http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf}} note = {\url{http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf}},
} }
\section{Changes} \section{Changes}
\subsection*{Version \version} \subsection*{Version \version}
\begin{itemize}
\item Update according to \acsl 1.16
\begin{itemize}
\item \changeinsection{fn-behavior}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\item \changeinsection{assertions}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\item \changeinsection{generalized-invariants}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\item \changeinsection{loop_annot}{add the \lstinline|check| and
\lstinline|admit| clause kinds}
\end{itemize}
\end{itemize}
\subsection*{Version 1.15}
\begin{itemize}
\item Update according to \acsl 1.15:
\begin{itemize}
\item \changeinsection{ghost}{add the \lstinline|\\ghost| qualifier}
\end{itemize}
\end{itemize}
\subsection*{Version 1.14}
\begin{itemize} \begin{itemize}
\item Update according to \acsl 1.14: \item Update according to \acsl 1.14:
\begin{itemize} \begin{itemize}
......
...@@ -3,7 +3,9 @@ ...@@ -3,7 +3,9 @@
{ decreases-clause? } simple-clause* { decreases-clause? } simple-clause*
named-behavior* completeness-clause* named-behavior* completeness-clause*
\ \
requires-clause ::= "requires" pred ";" clause-kind ::= "check" | { "admit" }
\
requires-clause ::= clause-kind? "requires" pred ";"
\ \
{ decreases-clause } ::= { "decreases" term ("for" id)? ";" } { decreases-clause } ::= { "decreases" term ("for" id)? ";" }
\ \
...@@ -16,7 +18,7 @@ ...@@ -16,7 +18,7 @@
\ \
{ location } ::= { tset } { location } ::= { tset }
\ \
ensures-clause ::= "ensures" pred ";" ensures-clause ::= clause-kind? "ensures" pred ";"
\ \
named-behavior ::= "behavior" id ":" behavior-body named-behavior ::= "behavior" id ":" behavior-body
\ \
......
% --------------------------------------------------------------------------
% --- LaTeX Class for Frama-C Books ---
% --------------------------------------------------------------------------
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
% --------------------------------------------------------------------------
% --- Base Class management ---
% --------------------------------------------------------------------------
\LoadClass[a4paper,11pt,twoside,openright]{report}
\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
\ProcessOptions
\RequirePackage{fullpage}
\RequirePackage{hevea}
\RequirePackage{ifthen}
\RequirePackage[T1]{fontenc}
\RequirePackage[latin1]{inputenc}
\RequirePackage[a4paper,pdftex,pdfstartview=FitH]{hyperref}
\RequirePackage{amssymb}
\RequirePackage{xcolor}
\RequirePackage[pdftex]{graphicx}
\RequirePackage{xspace}
\RequirePackage{makeidx}
\RequirePackage[leftbars]{changebar}
\RequirePackage[english]{babel}
\RequirePackage{fancyhdr}
\RequirePackage{titlesec}
% --------------------------------------------------------------------------
% --- 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{\setlength\unitlength{1cm}%
\begin{picture}(0,0)(#1,#2)
\put(0,0){\includegraphics{#3}}
\end{picture}}
\fancypagestyle{plain}{%
\fancyfoot{}
\fancyhead{}
\fancyhead[LE]{\put@bg(2.4,27.425){frama-c-left.pdf}}
\fancyhead[LO]{\put@bg(2.7,27.425){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){frama-c-left.pdf}}
\fancyhead[LO]{\put@bg(2.7,27.425){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,0){\includegraphics{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
}
% --------------------------------------------------------------------------
% --- Sectionning ---
% --------------------------------------------------------------------------
\titleformat{\chapter}[display]{\Huge\raggedleft}%
{\huge\chaptertitlename\,\thechapter}{0.5em}{}
\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
[\vspace{-14pt}\rule{\textwidth}{0.1pt}\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={assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
exit_behavior,ghost,global,inductive,integer,invariant,lemma,logic,loop,
model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
union,variant},
% otherkeywords={\\at,\\base_addr,\\block_length,\\false,\\fresh,\\from,
% \\initialized,\\lambda,\\let,\\match,\\max,\\nothing,\\null,
% \\numof,\\old,\\result,\\specified,\\strlen,\\sum,\\true,
% \\valid,\\valid_range},
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\scriptsize\else\normalfont\ttfamily\mdseries\scriptsize\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}{%
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={[is]{//NOPP-BEGIN}{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}}
\lstnewenvironment{listing}[2][1]%
{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
\lstnewenvironment{listing-nonumber}%
{\lstset{style=c,numbers=none,basicstyle=\lp