update figures

compcertoe/compcertoe.tex

@@ -4697,27 +4697,22 @@ \section{Evaluation and Applications} \label{sec:app} %{{{
     % Includes: anything under compcerto/ (is mem sep there also?)
     CompCertO & 124,217 & 95,187 &
     %
-    % Includes: ??
-      Memory Separation (\S\ref{sec:application:sepalg}) & ?? & ?? \\
+    % Includes: examples/clight/Join.v
+    Memory Separation (\S\ref{sec:application:sepalg}) & 258 & 893 \\
     %
     % Includes: structures/*.v lattices/*.v
     Other support code & 271 & 491 &
     %
-    % Includes: examples/process/*.v
-      Process example (\S\ref{sec:application:loader}) & 9,468 & 14,888 \\
+    % 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: 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/*.v
-      ClightP (\S\ref{sec:application:clightp}) & 5,745 & 9,152 \\
+    % Includes: examples/clightp/ClightP.v examples/clightp/ClightPComp.v examples/clightp/ClightPLink.v
+      ClightP (\S\ref{sec:application:clightp}) & 1,481 & 1,662 \\
     \bottomrule
-    % Not assigned:
-    %   examples/Determ.v
-    %   examples/Rot13.v
-    %   examples/SecretAsm.v
-    %   examples/Util.v
   \end{tabular}
 \end{table}
 %}}}