diff options
author | Nguyễn Gia Phong <cnx@loang.net> | 2023-12-01 16:25:25 +0900 |
---|---|---|
committer | Nguyễn Gia Phong <cnx@loang.net> | 2023-12-01 16:25:25 +0900 |
commit | 3285b6df66a9c3e0a6502ae75c93085f2d6a0f44 (patch) | |
tree | ab32447e5485d9946b82ccdbfed00a3650ba06e2 /bg.tex | |
parent | 679ca723e849b731a9d94a276763bb59756aa3a2 (diff) | |
download | thesis-3285b6df66a9c3e0a6502ae75c93085f2d6a0f44.tar.gz |
Snapshot current content
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} |