Index: Deliverables/D1.2/CompilerProofOutline/outline.tex
===================================================================
 Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1774)
+++ Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1775)
@@ 997,6 +997,7 @@
the CompCert project~\cite{compcert} for the CompCert pass that is closest to
ours; 3) an estimation of the complexity of the pass according to the
analysis above.

+analysis above. The result is shown in Table~\ref{table}.
+
+\begin{table}{h}
\begin{tabular}{lrlrr}
Pass origin & Code lines & CompCert ratio & Estimated effort & Estimated effort \\
@@ 1019,4 +1020,6 @@
Total & 14630 & 3.75 \permil & 49.30 & 54.0 \\
\end{tabular}
+\caption{\label{table}Estimated effort}
+\end{table}
We provide now some additional informations on the methodology used in the
@@ 1087,5 +1090,6 @@
less than 1/3rd of the total effort. At least half of this effort really goes
into simple data structures (vectors, bounded and unbounded integers, tries
and maps) whose certification is not very interesting and could be sacrificed.
+and maps) whose certification is not interesting and whose code could be
+taken without reproving it from the library of any other theorem prover.
\section{Conclusions}