diff --git a/compcertoe/compcertoe.tex b/compcertoe/compcertoe.tex index e080d4f..a5b3aba 100644 --- a/compcertoe/compcertoe.tex +++ b/compcertoe/compcertoe.tex @@ -4697,21 +4697,21 @@ \section{Evaluation and Applications} \label{sec:app} %{{{ % Includes: anything under compcerto/ (is mem sep there also?) CompCertO & 124,217 & 95,187 & % - % Includes: examples/clight/Join.v + % Includes: examples/clightp/Join.v Memory Separation (\S\ref{sec:application:sepalg}) & 258 & 893 \\ % % Includes: structures/*.v lattices/*.v Other support code & 271 & 491 & % - % Includes: examples/Rot13.v examples/process/InitMem.v examples/Util.v examples/SecretAsm.v - Process example (\S\ref{sec:application:loader}) & 1,086 & 2,346 \\ + % Includes: examples/Rot13.v examples/Util.v examples/SecretAsm.v examples/process/*.v + Process example (\S\ref{sec:application:loader}) & 1,712 & 2,961 \\ % % Includes: models/IntStrat.v Our framework (\S\ref{sec:overview}--\ref{sec:scomp}, \S\ref{sec:application:impl}) \hspace{-1em} & 2,198 & 3,252 & % - % Includes: examples/clightp/ClightP.v examples/clightp/ClightPComp.v examples/clightp/ClightPLink.v - ClightP (\S\ref{sec:application:clightp}) & 1,481 & 1,662 \\ + % Includes: examples/clightp/*.v except Join.v + CAL and ClightP (\S\ref{sec:application:cal}, \S\ref{sec:application:clightp}) & 4,285 & 7,285 \\ \bottomrule \end{tabular} \end{table}