blob: 0ba8e659cf6e72f8d8dcd40e6e0322a12d5e0133 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
\providecommand\saildoclabelled[2]{\phantomsection\label{#1}#2}
\providecommand\saildocval[2]{#1 #2}
\providecommand\saildocfcl[2]{#1 #2}
\providecommand\saildoctype[2]{#1 #2}
\providecommand\saildocfn[2]{#1 #2}
\providecommand\saildocoverload[2]{#1 #2}
\newcommand{\sailtypeast}{\saildoclabelled{sailtypezast}{\saildoctype{}{\lstinputlisting[language=sail]{out/typezast6bb070d12e82e4887160cdfd016230c8.tex}}}}
\newcommand{\sailvalexecute}{\saildoclabelled{sailzexecute}{\saildocval{}{\lstinputlisting[language=sail]{out/valzexecute33a689e3a631b9b905b85461d3814943.tex}}}}
\newcommand{\sailfclCAndPermBrokenexecute}{\saildoclabelled{sailfclCAndPermBrokenzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability
register \emph{cs1} with the \cperms{} field set to the bitwise-AND of
its previous value and bits 0 .. 10 of integer register \emph{rs2}
and the \cuperms{} field set to the bitwise and of its previous value
and bits \hyperref\hyperref[sailztablezGpseudocodezDconstants]{\lstinline{table:pseudocode-constants}}{\emph{first\_uperm}} ..
\hyperref\hyperref[sailztablezGpseudocodezDconstants]{\lstinline{table:pseudocode-constants}}{\emph{last\_uperm}} of \emph{rd}.
}{\lstinputlisting[language=sail]{out/fclCAndPermBrokenzexecute33a689e3a631b9b905b85461d3814943.tex}}}}
\newcommand{\sailfclCAndPermEscapedexecute}{\saildoclabelled{sailfclCAndPermEscapedzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability
register \emph{cs1} with the \cperms{} field set to the bitwise-AND of
its previous value and bits 0 .. 10 of integer register \emph{rs2}
and the \cuperms{} field set to the bitwise and of its previous value
and bits \hyperref[table:pseudocode-constants]{\emph{first\_uperm}} ..
\hyperref[table:pseudocode-constants]{\emph{last\_uperm}} of \emph{rd}.
}{\lstinputlisting[language=sail]{out/fclCAndPermEscapedzexecute33a689e3a631b9b905b85461d3814943.tex}}}}
\newcommand{\sailfclCAndPermMarkdownexecute}{\saildoclabelled{sailfclCAndPermMarkdownzexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability
register \emph{cs1} with the \cperms{} field set to the bitwise-AND of
its previous value and bits 0 .. 10 of integer register \emph{rs2}
and the \cuperms{} field set to the bitwise and of its previous value
and bits \hyperref[table:pseudocode-constants]{*first_uperm*} ..
\hyperref[table:pseudocode-constants]{*last_uperm*} of \emph{rd}.
}{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownzexecute33a689e3a631b9b905b85461d3814943.tex}}}}
\newcommand{\sailfclCAndPermMarkdownWithRefMacroexecute}{\saildoclabelled{sailfclCAndPermMarkdownWithRefMacrozexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability
register \emph{cs1} with the \cperms{} field set to the bitwise-AND of
its previous value and bits 0 .. 10 of integer register \emph{rs2}
and the \cuperms{} field set to the bitwise and of its previous value
and bits \firstUPerm{} .. \lastUPerm{} of \emph{rd}.
}{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithRefMacrozexecute33a689e3a631b9b905b85461d3814943.tex}}}}
\newcommand{\sailfclCAndPermMarkdownWithExceptionsexecute}{\saildoclabelled{sailfclCAndPermMarkdownWithExceptionszexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability
register \emph{cs1} with the \cperms{} field set to the bitwise-AND of
its previous value and bits 0 .. 10 of integer register \emph{rs2}
and the \cuperms{} field set to the bitwise and of its previous value
and bits \firstUPerm{} .. \lastUPerm{} of \emph{rd}.
\subsubsection*{Exceptions:}
An exception is raised if:
\begin{itemize}
\item \emph{cs1.tag} is not set.
\item \emph{cs1} is sealed.
\end{itemize}
}{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithExceptionszexecute33a689e3a631b9b905b85461d3814943.tex}}}}
\newcommand{\sailval}[1]{
\ifstrequal{#1}{execute}{\sailvalexecute}{}}
\newcommand{\sailrefval}[2]{
\ifstrequal{#1}{execute}{\hyperref[sailzexecute]{#2}}{}}
\newcommand{\sailfn}[1]{
}
\newcommand{\sailreffn}[2]{
}
\newcommand{\sailtype}[1]{
\ifstrequal{#1}{ast}{\sailtypeast}{}}
\newcommand{\sailreftype}[2]{
\ifstrequal{#1}{ast}{\hyperref[sailtypezast]{#2}}{}}
|
