diff options
Diffstat (limited to 'verilog.tex')
| -rw-r--r-- | verilog.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/verilog.tex b/verilog.tex index 1e0b9ff..11087b0 100644 --- a/verilog.tex +++ b/verilog.tex @@ -92,7 +92,7 @@ The \compcert{} computation model defines a set of states through which executio \compcert{} executions pass through three main states: \begin{description} \item[\texttt{State} $\mathit{sf}$ $m$ $v$ $\Gamma_{r}$ $\Gamma_{a}$] The main state when executing a function, with stack frame $\mathit{sf}$, current module $m$, current state $v$ and variable states $\Gamma_{r}$ and $\Gamma_{a}$. - \item[\texttt{Callstate} $\mathit{sf}$ ${r}$] The state that is reached when a function is called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$. + \item[\texttt{Callstate} $\mathit{sf}$ $m$ $\vec{r}$] The state that is reached when a function is called, with the current stack frame $\mathit{sf}$, current module $m$ and arguments $\vec{r}$. \item[\texttt{Returnstate} $\mathit{sf}$ $v$] The state that is reached when a function returns back to the caller, with stack frame $\mathit{sf}$ and return value $v$. \end{description} |