From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Util/latex/boogie.sty | 242 +++++++++++++++++++++++++-------------------------
 1 file changed, 121 insertions(+), 121 deletions(-)

(limited to 'Util/latex/boogie.sty')

diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty
index e67c61f4..65fa7fb1 100644
--- a/Util/latex/boogie.sty
+++ b/Util/latex/boogie.sty
@@ -1,121 +1,121 @@
-% boogie.sty
-% Boogie mode for the LaTeX listings package.
-% Rustan Leino, 30 May 2008.
-% Example:
-% \begin{boogie}
-% type Field \alpha;
-% var Heap: <<\alpha>>[ref, Field \alpha]\alpha where IsHeap(Heap);
-% function IsHeap(<<\alpha>>[ref, Field \alpha]\alpha) returns (bool);
-% procedure Inc(x: int) returns (y: int)
-%   modifies Heap;
-% {
-%   havoc Heap;
-%   if (0 <= x && x < 100) {
-%     y := x + 1;
-%   }
-% }
-% \end{boogie}
-
-\usepackage{listings}
-
-\lstdefinelanguage{boogie}{
-  morekeywords={type,bool,int,real,%
-      bv0,bv1,bv2,bv3,bv4,bv5,bv6,bv7,bv8,bv9,%
-      bv10,bv11,bv12,bv13,bv14,bv15,bv16,bv17,bv18,bv19,%
-      bv20,bv21,bv22,bv23,bv24,bv25,bv26,bv27,bv28,bv29,%
-      bv30,bv31,bv32,bv33,bv34,bv35,bv36,bv37,bv38,bv39,%
-      bv40,bv41,bv42,bv43,bv44,bv45,bv46,bv47,bv48,bv49,%
-      bv50,bv51,bv52,bv53,bv54,bv55,bv56,bv57,bv58,bv59,%
-      bv60,bv61,bv62,bv63,bv64,% ...
-      const,unique,complete,partition,
-      axiom,
-      function,returns,
-      var,where,
-      procedure,implementation,
-      requires,modifies,ensures,free,
-      % expressions
-      false,true,null,old,then,div,mod,
-      % statements
-      assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
-      },
-  literate=%
-    {:}{$\colon$}1
-    {::}{$\bullet$}2
-    {:=}{$:$$=$}2
-    {!}{$\lnot$}1
-    {==}{$=$}1
-    {!=}{$\neq$}1
-    {&&}{$\land$}1
-    {||}{$\lor$}1
-    {<=}{$\le$}1
-    {>=}{$\ge$}1
-    {==>}{$\Longrightarrow$}3 
-    {<==>}{$\Longleftrightarrow$}4 
-    {forall}{$\forall$}1
-    {exists}{$\exists$}1
-    {lambda}{$\lambda$}1
-    % the following isn't actually Boogie, but it gives the option to produce nicer latex
-    {<<}{$\langle$}1
-    {>>}{$\rangle$}1
-    {\\alpha}{$\alpha$}1
-    {\\beta}{$\beta$}1
-    {\\gamma}{$\gamma$}1
-    {\\delta}{$\delta$}1
-    {\\epsilon}{$\epsilon$}1
-    {\\zeta}{$\zeta$}1
-    {\\eta}{$\eta$}1
-    {\\theta}{$\theta$}1
-    {\\iota}{$\iota$}1
-    {\\kappa}{$\kappa$}1
-    {\\lambda}{$\lambda$}1
-    {\\mu}{$\mu$}1
-    {\\nu}{$\nu$}1
-    {\\xi}{$\xi$}1
-    {\\pi}{$\pi$}1
-    {\\rho}{$\rho$}1
-    {\\sigma}{$\sigma$}1
-    {\\tau}{$\tau$}1
-    {\\upsilon}{$\upsilon$}1
-    {\\phi}{$\phi$}1
-    {\\chi}{$\chi$}1
-    {\\psi}{$\psi$}1
-    {\\omega}{$\omega$}1
-    {\\Gamma}{$\Gamma$}1
-    {\\Delta}{$\Delta$}1
-    {\\Theta}{$\Theta$}1
-    {\\Lambda}{$\Lambda$}1
-    {\\Xi}{$\Xi$}1
-    {\\Pi}{$\Pi$}1
-    {\\Sigma}{$\Sigma$}1
-    {\\Upsilon}{$\Upsilon$}1
-    {\\Phi}{$\Phi$}1
-    {\\Psi}{$\Psi$}1
-    {\\Omega}{$\Omega$}1
-    ,
-  sensitive=true,  % case sensitive
-  morecomment=[l]{//},
-  morecomment=[s]{/*}{*/},
-  morestring=[b]",
-  numbers=none,
-  firstnumber=0,
-  numberstyle=\tiny,
-  stepnumber=5,
-  basicstyle=\scriptsize\sffamily,
-  commentstyle=\itshape,
-  keywordstyle=\bfseries,
-  ndkeywordstyle=\bfseries,
-}
-\lstnewenvironment{boogie}[1][]{%
-  \lstset{language=boogie,
-    floatplacement={tbp},captionpos=b,
-    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
-\lstnewenvironment{boogieNoLines}[1][]{%
-  \lstset{language=boogie,
-    floatplacement={tbp},captionpos=b,
-    xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
-\def\inlineboogie{%
-    \lstinline[language=boogie,basicstyle=\ttfamily,columns=fixed]}
-\newcommand{\lstfile}[1]{
-  \lstinputlisting[language=boogie,%
-    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}
-}
+% boogie.sty
+% Boogie mode for the LaTeX listings package.
+% Rustan Leino, 30 May 2008.
+% Example:
+% \begin{boogie}
+% type Field \alpha;
+% var Heap: <<\alpha>>[ref, Field \alpha]\alpha where IsHeap(Heap);
+% function IsHeap(<<\alpha>>[ref, Field \alpha]\alpha) returns (bool);
+% procedure Inc(x: int) returns (y: int)
+%   modifies Heap;
+% {
+%   havoc Heap;
+%   if (0 <= x && x < 100) {
+%     y := x + 1;
+%   }
+% }
+% \end{boogie}
+
+\usepackage{listings}
+
+\lstdefinelanguage{boogie}{
+  morekeywords={type,bool,int,real,%
+      bv0,bv1,bv2,bv3,bv4,bv5,bv6,bv7,bv8,bv9,%
+      bv10,bv11,bv12,bv13,bv14,bv15,bv16,bv17,bv18,bv19,%
+      bv20,bv21,bv22,bv23,bv24,bv25,bv26,bv27,bv28,bv29,%
+      bv30,bv31,bv32,bv33,bv34,bv35,bv36,bv37,bv38,bv39,%
+      bv40,bv41,bv42,bv43,bv44,bv45,bv46,bv47,bv48,bv49,%
+      bv50,bv51,bv52,bv53,bv54,bv55,bv56,bv57,bv58,bv59,%
+      bv60,bv61,bv62,bv63,bv64,% ...
+      const,unique,complete,partition,
+      axiom,
+      function,returns,
+      var,where,
+      procedure,implementation,
+      requires,modifies,ensures,free,
+      % expressions
+      false,true,null,old,then,div,mod,
+      % statements
+      assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
+      },
+  literate=%
+    {:}{$\colon$}1
+    {::}{$\bullet$}2
+    {:=}{$:$$=$}2
+    {!}{$\lnot$}1
+    {==}{$=$}1
+    {!=}{$\neq$}1
+    {&&}{$\land$}1
+    {||}{$\lor$}1
+    {<=}{$\le$}1
+    {>=}{$\ge$}1
+    {==>}{$\Longrightarrow$}3 
+    {<==>}{$\Longleftrightarrow$}4 
+    {forall}{$\forall$}1
+    {exists}{$\exists$}1
+    {lambda}{$\lambda$}1
+    % the following isn't actually Boogie, but it gives the option to produce nicer latex
+    {<<}{$\langle$}1
+    {>>}{$\rangle$}1
+    {\\alpha}{$\alpha$}1
+    {\\beta}{$\beta$}1
+    {\\gamma}{$\gamma$}1
+    {\\delta}{$\delta$}1
+    {\\epsilon}{$\epsilon$}1
+    {\\zeta}{$\zeta$}1
+    {\\eta}{$\eta$}1
+    {\\theta}{$\theta$}1
+    {\\iota}{$\iota$}1
+    {\\kappa}{$\kappa$}1
+    {\\lambda}{$\lambda$}1
+    {\\mu}{$\mu$}1
+    {\\nu}{$\nu$}1
+    {\\xi}{$\xi$}1
+    {\\pi}{$\pi$}1
+    {\\rho}{$\rho$}1
+    {\\sigma}{$\sigma$}1
+    {\\tau}{$\tau$}1
+    {\\upsilon}{$\upsilon$}1
+    {\\phi}{$\phi$}1
+    {\\chi}{$\chi$}1
+    {\\psi}{$\psi$}1
+    {\\omega}{$\omega$}1
+    {\\Gamma}{$\Gamma$}1
+    {\\Delta}{$\Delta$}1
+    {\\Theta}{$\Theta$}1
+    {\\Lambda}{$\Lambda$}1
+    {\\Xi}{$\Xi$}1
+    {\\Pi}{$\Pi$}1
+    {\\Sigma}{$\Sigma$}1
+    {\\Upsilon}{$\Upsilon$}1
+    {\\Phi}{$\Phi$}1
+    {\\Psi}{$\Psi$}1
+    {\\Omega}{$\Omega$}1
+    ,
+  sensitive=true,  % case sensitive
+  morecomment=[l]{//},
+  morecomment=[s]{/*}{*/},
+  morestring=[b]",
+  numbers=none,
+  firstnumber=0,
+  numberstyle=\tiny,
+  stepnumber=5,
+  basicstyle=\scriptsize\sffamily,
+  commentstyle=\itshape,
+  keywordstyle=\bfseries,
+  ndkeywordstyle=\bfseries,
+}
+\lstnewenvironment{boogie}[1][]{%
+  \lstset{language=boogie,
+    floatplacement={tbp},captionpos=b,
+    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
+\lstnewenvironment{boogieNoLines}[1][]{%
+  \lstset{language=boogie,
+    floatplacement={tbp},captionpos=b,
+    xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
+\def\inlineboogie{%
+    \lstinline[language=boogie,basicstyle=\ttfamily,columns=fixed]}
+\newcommand{\lstfile}[1]{
+  \lstinputlisting[language=boogie,%
+    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}
+}
-- 
cgit v1.2.3