[doc] minor

doc/frama-c-book.cls

@@ -430,7 +430,7 @@
 \def\lp@string{\color{frama-c-dark-green}} \def\lp@ident{}
 \def\lp@number{\rmfamily\tiny\color{lstnum}\noncopynumber}
 
-\lstdefinestyle{frama-c-style}{%
+\lstdefinestyle{frama-c-basic-style}{%
   captionpos=b,%
   columns=flexible,%
   basicstyle=\lp@inline,%
@@ -448,28 +448,22 @@
   framerule=1pt,%
   rulecolor=\color{frama-c-orange!60},%
   backgroundcolor=\color{frama-c-bronze!10},%
+  literate={\ }{\ }1,
+  % ^~~~~  Without this, spaces starting a line does not have the right size ...
+}
+
+\lstdefinestyle{frama-c-style}{%
+  style=frama-c-basic-style,%
   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=`,
-  literate={\ }{\ }1
-  % ^~~~~  Without this, spaces starting a line does not have the right size ...
 }
 
 % Code styles
 % --------------------------------------------------------------------------
 
-\lstdefinestyle{framac-code-style}{%
-  basicstyle=\lp@inline,%
-  keywordstyle=[1]\sffamily\color{lstmodule},%
-  keywordstyle=[2]\sffamily\color{lstspecial},%
-  keywordstyle=[3]\sffamily\bfseries,%
-  identifierstyle=\rmfamily,%
-  stringstyle=\ttfamily\color{frama-c-orange},%
-  commentstyle=\rmfamily\bfseries\color{lsttxt},%
-}
 \lstdefinestyle{framac-shell-style}{%
   mathescape=false,%
   basicstyle=\lp@basic,%
@@ -529,20 +523,19 @@
 % --------------------------------------------------------------------------
 
 \lstdefinestyle{framac-code}%
-{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
+{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
 
 \newcommand{\cinput}[2][]%
 {\lstinputlisting[
     language={[ANSI]C},
     alsolanguage=ACSL,
-    style=framac-code-style,basicstyle=
-    \lp@basic,#1]{#2}
+    style=frama-c-style,#1]{#2}
 }
 \newcommand{\cinline}[1]%
 {\lstinline[style=framac-code]{#1}}
 
 \lstnewenvironment{ccode}[1][]%
-{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
+{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic,#1}}{}
 
 % Configure
 % --------------------------------------------------------------------------
@@ -566,7 +559,7 @@
     {à}{{\`a}}1%
     {é}{{\'e}}1%
   ,
-  style=framac-code-style,%
+  style=frama-c-style,%
   morekeywords={
     action, alias, as, deps, dune, executable, files, flags, from,
     generate_opam_files, install, lang, libraries, library, name, optional,
@@ -582,7 +575,7 @@
 
 \lstdefinestyle{dune-basic}{%
   language=Dune,%
-  style=framac-code-style,%
+  style=frama-c-basic-style,%
   basicstyle=\lp@inline,%
 }
 
@@ -614,7 +607,7 @@
 
 \lstdefinestyle{make-basic}{%
   language=Makefile,%
-  style=framac-code-style,%
+  style=frama-c-basic-style,%
   basicstyle=\lp@inline,%
 }
 
@@ -631,7 +624,7 @@
 % --------------------------------------------------------------------------
 
 \lstdefinelanguage{Ocaml}[Objective]{Caml}{%
-  style=framac-code-style,%
+  style=frama-c-basic-style,%
   deletekeywords={when,module,struct,sig,begin,end},%
   morekeywords=[2]{failwith,raise,when},%
   morekeywords=[3]{module,struct,sig,begin,end},%
@@ -702,7 +695,7 @@
 
 \lstdefinestyle{why-style}{%
   language=Why,%
-  style=framac-code-style,%
+  style=frama-c-basic-style,%
   basicstyle=\lp@inline,%
 }
 

doc/metrics/metrics.tex

@@ -114,7 +114,7 @@ this purpose. }.
 \end{shell}
 \begin{figure}
   \centering
-  \lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,
+  \lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,
   basicstyle=\lp@basic,firstline=5]
   {../../tests/metrics/\pgname}
   \caption{Source code for \pgname}

doc/userman/user-analysis.tex

@@ -56,12 +56,12 @@ All \FramaC plug-ins define the following set of common options.
   \optionidxdef{-}{<plug-in>-msg-key}
   \optionidxdef{-}{kernel-msg-key}
   sets the categories of
-  messages that must be output for the plugin. \texttt{keys} is a 
-  comma-separated list of names. The list of available categories can be 
+  messages that must be output for the plugin. \texttt{keys} is a
+  comma-separated list of names. The list of available categories can be
   obtained with \texttt{-<plug-in shortname>-msg-key help}. To enable all
   categories, use the wildcard \texttt{'*'}%
   \footnote{Be sure to enclose it in single quotes or your shell might
-    expand it, leading to unexpected results.}. Categories can have 
+    expand it, leading to unexpected results.}. Categories can have
   subcategories, defined by a colon in their names. For instance, \texttt{a:b:c}
   is a subcategory \texttt{c} of \texttt{a:b}, itself a
   subcategory of \texttt{a}. Enabling a category will also enable all its
@@ -216,13 +216,13 @@ short truncate(int n) {
 }
 \end{ccode}
 If \texttt{-warn-signed-downcast} is set, analyzers report an error on
-{\lstset{language=C,style=framac-code-style} \lstinline|(short) n|}
+{\lstset{language=C,style=frama-c-style} \lstinline|(short) n|}
 which downcasts a signed integer to a signed
 short. Without it, no error is reported.
 
 \item \optiondef{-}{warn-unsigned-downcast} is the same as
   \texttt{-warn-signed-downcast} for downcasts to unsigned integers. This option
-  is also \emph{not} set by default. 
+  is also \emph{not} set by default.
 
 \item \optiondef{-}{warn-signed-overflow} may be used to check that the
   analyzed code does not overflow on integer operations. If the opposite option
@@ -240,7 +240,7 @@ int abs(int x) {
 By default, analyzers detect an error on
 \lstinline|-x| since this operation overflows when \lstinline|MININT| is the
 argument of the function. But, with the \texttt{-no-warn-signed-overflow}
-option, no error is detected.  
+option, no error is detected.
 
 \item \optiondef{-}{warn-unsigned-overflow} is the same as
   \texttt{-warn-signed-overflow} for operations over unsigned integers. This
@@ -280,4 +280,4 @@ option, no error is detected.
 % TeX-master: "userman.tex"
 % ispell-local-dictionary: "english"
 % compile-command: "make"
-% End: 
+% End: