pinipushto

Author: Aslan Askarov

body.tex

@@ -841,15 +841,6 @@ \subsubsection{\code{getTime}}
 \end{description}
 
 
-\subsubsection{\code{getTime}}
-\begin{description}
-    \item [Description] Obtains current Unix timestmap
-    \item [Arguments] Unit.
-    \item [Returns] Number. 
-    \item [Example usage] \textcode{getTime()}
-\end{description}
-
-
 \subsubsection{\code{inputLine}}
 \begin{description}
 \item[Description] Reads a  line from the console.
@@ -910,6 +901,18 @@ \subsubsection{\code{pinipush}}
     \item [Example usage] \textcode{pinipush (authority)}
 \end{description}
 
+
+\subsubsection{\code{pinipushto}}
+\begin{description}
+    \item [Description] Pushes authority value onto the \emph{pini} stack,
+	 with explicit blocking level. 
+    \item [Arguments] A tuple: a value of type authority, and a level.
+    \item [Returns] A string capability to be passed as the argument to \code{pinipop}
+    \item [Failure behavior] Crashes if the current blocking level does not flow to the level argument.
+    \item [Example usage] \textcode{pinipushto (authority, {bob})}
+\end{description}
+
+
 \subsubsection{\code{print}}
 \begin{description}
     \item [Description] Prints a value on the console omitting its security types.

main.tex

@@ -39,7 +39,7 @@
 %\author{}
 % \author{\sf Aslan Askarov \\ \small aslan@cs.au.dk}
 
-\date{March 16, 2020}  % Activate to display a given date or no date
+\date{March 26, 2020}  % Activate to display a given date or no date
 
 \begin{document}
 \maketitle