diff options
Diffstat (limited to 'bg.tex')
| -rw-r--r-- | bg.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/bg.tex b/bg.tex index 4c12048..b1845d4 100644 --- a/bg.tex +++ b/bg.tex @@ -66,6 +66,7 @@ Marking can be communicated either through command-line options for files (including standard streams) and command-line arguments or via in-source annotations~\cite{klee-docs}. + As shown in algorithm~\ref{symb-exec}, the path constraints is only expanded at branching instructions, so only values affecting the control flow are tracked, since \klee{} targets the exploration of execution paths. @@ -74,7 +75,8 @@ involving such value must be artificially injected. One common idiom for doing this condition injection~\cite{angelix,cpr,trident} is shown in figure~\ref{klee-output}. There, a~temporary symbolic avatar \texttt{var} is created for the sole purpose of being fixed to the value \texttt{val} -in the path constraints. +in the path constraints. From here, this mechanism shall be referred to +in abstract descriptions as \textsc{SymbolicOutput(value, context)}. \begin{figure}[h]\centering\hfill \begin{subfigure}{0.6\textwidth} |