Skip to content

Commit

Permalink
update figures
Browse files Browse the repository at this point in the history
  • Loading branch information
Yu-zh committed Oct 26, 2024
1 parent 68f538f commit 8882db8
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions compcertoe/compcertoe.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down

0 comments on commit 8882db8

Please sign in to comment.