# Changeset 1742 for Deliverables/D1.2

Ignore:
Timestamp:
Feb 24, 2012, 3:40:52 PM (9 years ago)
Message:
• committed new version of effort table
File:
1 edited

Unmodified
Added
Removed
• ## Deliverables/D1.2/CompilerProofOutline/outline.tex

 r1741 \section{Estimated effort} Based on the rough analysis performed so far we can now estimate the total effort for the certification of the compiler. We obtain the estimation by Based on the rough analysis performed so far we can estimate the total effort for the certification of the compiler. We obtain this estimation by combining, for each pass: 1) the number of lines of code to be certified; 2) the ratio number of lines of proof on number of lines of code from CompCert project~\cite{compcert} for the CompCert pass that is closer to 2) the ratio of number of lines of proof to number of lines of code from 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. Clight & \\ Cminor & \\ RTLabs & 1252 & 1.17 \permil & 1.5 \\ RTL    &  469 & 2.90 \permil & 1.4 \\ ERTL   &  789 & 2.79 \permil & 2.2 \\ LTL    &      & \\ LIN    &  354 & 7.34 \permil & 2.6 \\ ASM    &      & \\ RTLabs & 1252 & 1.17 \permil & 1.48 \\ RTL    &  469 & 4.17 \permil & 1.95 \\ ERTL   &  789 & 3.01 \permil & 2.38 \\ LTL    &   92 & 5.94 \permil & 0.55 \\ LIN    &  354 & 4.80 \permil & 1.70 \\ ASM    &  984 & 6.54 \permil & 6.44 \\ \end{tabular}
Note: See TracChangeset for help on using the changeset viewer.