Changeset 1753 for Deliverables/D1.2

Timestamp:

Feb 24, 2012, 5:36:38 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (3 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -629 +629 @@
 $$
 \begin{array}{lL>{(ex. $}L<{)$}}
-\Defined(s) & registers defined at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \mathtt{CALL}id\mapsto \text{caller-save}
+\Defined(s) & registers defined at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_1,C\}, \mathtt{CALL}~id\mapsto \text{caller-save}
 \\
-\Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \mathtt{CALL}id\mapsto \text{parameters}
+\Used(s) & registers used at $s$ & r_1\leftarrow r_2+r_3 \mapsto \{r_2,r_3\}, \mathtt{CALL}~id\mapsto \text{parameters}
 \end{array}
 $$
@@ -761 +761 @@
             &            &                & (based on CompCert) & \\
 \hline
-Common & 12759 & 4.25 \permil & 54.22 \\
+Common &  4864 & 4.25 \permil & 20.67 \\
 Cminor &  1057 & 5.23 \permil & 5.53 \\
 Clight &  1856 & 5.23 \permil & 9.71 \\ 
@@ -771 +771 @@
 ASM    &   984 & 4.80 \permil & 4.72 \\
 \hline
-Total common    & 12759 & 4.25 \permil & 54.22 \\
+Total common    &  4864 & 4.25 \permil & 20.67 \\
 Total front-end &  2913 & 5.23 \permil & 15.24 \\
 Total back-end  &  6853 & 4.17 \permil & 13.39 \\
 \hline
-Total           & 22525 & 3.75 \permil & 84.85 \\
+Total           & 14630 & 3.75 \permil & 49.30 \\
 \end{tabular}