Changeset 1982


Ignore:
Timestamp:
May 22, 2012, 8:14:57 AM (5 years ago)
Author:
amadio
Message:

add 2.1 Survey

Location:
Deliverables/D2.1
Files:
2 added
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.1/report.aux

    r59 r1982  
    2626\citation{W09}
    2727\citation{Frama-C}
    28 \@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{5}{section.1}}
    29 \newlabel{intro-sec}{{1}{5}{Introduction\relax }{section.1}{}}
    30 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Meaning of cost annotations}{5}{subsection.1.1}}
    31 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Soundness and precision of cost annotations}{6}{subsection.1.2}}
    32 \@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Compositionality}{6}{subsection.1.3}}
    33 \newlabel{comp-intro}{{1.3}{6}{Compositionality\relax }{subsection.1.3}{}}
    34 \@writefile{toc}{\contentsline {subsection}{\numberline {1.4}Direct approach to cost annotations}{6}{subsection.1.4}}
    35 \newlabel{direct-intro}{{1.4}{6}{Direct approach to cost annotations\relax }{subsection.1.4}{}}
    36 \@writefile{toc}{\contentsline {subsection}{\numberline {1.5}Labelling approach to cost annotations}{7}{subsection.1.5}}
    37 \newlabel{label-intro}{{1.5}{7}{Labelling approach to cost annotations\relax }{subsection.1.5}{}}
    38 \newlabel{STEP1}{{1}{7}{Labelling approach to cost annotations\relax }{equation.1.1}{}}
    39 \citation{CIL02}
    40 \citation{Pottier}
    41 \newlabel{step2}{{2}{8}{Labelling approach to cost annotations\relax }{equation.1.2}{}}
    42 \@writefile{toc}{\contentsline {subsection}{\numberline {1.6}A toy compiler}{8}{subsection.1.6}}
    43 \newlabel{toy-intro}{{1.6}{8}{A toy compiler\relax }{subsection.1.6}{}}
    44 \@writefile{toc}{\contentsline {subsection}{\numberline {1.7}A C compiler}{8}{subsection.1.7}}
    45 \newlabel{Ccompiler-intro}{{1.7}{8}{A C compiler\relax }{subsection.1.7}{}}
    46 \@writefile{toc}{\contentsline {subsection}{\numberline {1.8}Organisation}{9}{subsection.1.8}}
    47 \@writefile{toc}{\contentsline {section}{\numberline {2}A toy compiler}{9}{section.2}}
    48 \newlabel{toy-compiler-sec}{{2}{9}{A toy compiler\relax }{section.2}{}}
    49 \@writefile{toc}{\contentsline {subsection}{\numberline {2.1}{\sf  Imp}: language and semantics}{9}{subsection.2.1}}
    50 \newlabel{imp-sec}{{2.1}{9}{\imp : language and semantics\relax }{subsection.2.1}{}}
    51 \@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Big-step semantics}{9}{subsection.2.2}}
    52 \citation{Leroy09-ln}
    53 \@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Big-step operational semantics of ${\sf  Imp}$}}{10}{table.1}}
    54 \newlabel{semantics-imp}{{1}{10}{Big-step operational semantics of $\imp $\relax }{table.1}{}}
    55 \@writefile{lot}{\contentsline {table}{\numberline {2}{\ignorespaces Small-step operational semantics of ${\sf  Imp}$ commands}}{10}{table.2}}
    56 \newlabel{small-step-imp}{{2}{10}{Small-step operational semantics of $\imp $ commands\relax }{table.2}{}}
    57 \@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Small-step semantics}{10}{subsection.2.3}}
    58 \@writefile{lot}{\contentsline {table}{\numberline {3}{\ignorespaces Operational semantics ${\sf  Vm}$ programs}}{11}{table.3}}
    59 \newlabel{semantics-vm}{{3}{11}{Operational semantics $\vm $ programs\relax }{table.3}{}}
    60 \@writefile{toc}{\contentsline {subsection}{\numberline {2.4}{\sf  Vm}: language and semantics}{11}{subsection.2.4}}
    61 \newlabel{vm-sec}{{2.4}{11}{\vm : language and semantics\relax }{subsection.2.4}{}}
    62 \newlabel{unicity-height-prop}{{2}{11}{\vm : language and semantics\relax }{theorem.2}{}}
    63 \citation{Leroy09-ln}
    64 \citation{MP67}
    65 \@writefile{lot}{\contentsline {table}{\numberline {4}{\ignorespaces Conditions for well-formed code}}{12}{table.4}}
    66 \newlabel{well-formed-instr}{{4}{12}{Conditions for well-formed code\relax }{table.4}{}}
    67 \@writefile{lot}{\contentsline {table}{\numberline {5}{\ignorespaces Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}}{12}{table.5}}
    68 \newlabel{compil-imp-vm}{{5}{12}{Compilation from $\imp $ to $\vm $\relax }{table.5}{}}
    69 \@writefile{toc}{\contentsline {subsection}{\numberline {2.5}Compilation from ${\sf  Imp}$ to ${\sf  Vm}$}{12}{subsection.2.5}}
    70 \newlabel{compil-imp-vm-sec}{{2.5}{12}{Compilation from $\imp $ to $\vm $\relax }{subsection.2.5}{}}
    71 \@writefile{toc}{\contentsline {subsection}{\numberline {2.6}Soundness of compilation for the big-step semantics}{12}{subsection.2.6}}
    72 \newlabel{soundness-big-step-prop}{{3}{12}{Soundness of compilation for the big-step semantics\relax }{theorem.3}{}}
    73 \@writefile{toc}{\contentsline {subsection}{\numberline {2.7}Soundness of compilation for the small-step semantics}{12}{subsection.2.7}}
    74 \citation{Larus05}
    75 \newlabel{soundness-small-step}{{4}{13}{Soundness of compilation for the small-step semantics\relax }{theorem.4}{}}
    76 \@writefile{toc}{\contentsline {subsection}{\numberline {2.8}Compiled code is well-formed}{13}{subsection.2.8}}
    77 \newlabel{well-formed-prop}{{5}{13}{Compiled code is well-formed\relax }{theorem.5}{}}
    78 \@writefile{toc}{\contentsline {subsection}{\numberline {2.9}${\sf  Mips}$: language and semantics}{13}{subsection.2.9}}
    79 \newlabel{mips-sec}{{2.9}{13}{$\mips $: language and semantics\relax }{subsection.2.9}{}}
    80 \@writefile{lot}{\contentsline {table}{\numberline {6}{\ignorespaces Operational semantics ${\sf  Mips}$ programs}}{14}{table.6}}
    81 \newlabel{semantics-mips}{{6}{14}{Operational semantics $\mips $ programs\relax }{table.6}{}}
    82 \@writefile{toc}{\contentsline {subsection}{\numberline {2.10}Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}{14}{subsection.2.10}}
    83 \newlabel{compil-vm-mips-sec}{{2.10}{14}{Compilation from $\vm $ to $\mips $\relax }{subsection.2.10}{}}
    84 \newlabel{p-function}{{3}{14}{Compilation from $\vm $ to $\mips $\relax }{equation.2.3}{}}
    85 \newlabel{d-function}{{4}{14}{Compilation from $\vm $ to $\mips $\relax }{equation.2.4}{}}
    86 \newlabel{simulation-vm-mips}{{6}{14}{Compilation from $\vm $ to $\mips $\relax }{theorem.6}{}}
    87 \@writefile{toc}{\contentsline {section}{\numberline {3}Direct approach for the toy compiler}{14}{section.3}}
    88 \newlabel{toy-direct-sec}{{3}{14}{Direct approach for the toy compiler\relax }{section.3}{}}
    89 \@writefile{lot}{\contentsline {table}{\numberline {7}{\ignorespaces Compilation from ${\sf  Vm}$ to ${\sf  Mips}$}}{15}{table.7}}
    90 \newlabel{compil-vm-mips}{{7}{15}{Compilation from $\vm $ to $\mips $\relax }{table.7}{}}
    91 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}${\sf  Mips}$ and ${\sf  Vm}$ cost annotations}{15}{subsection.3.1}}
    92 \@writefile{lot}{\contentsline {table}{\numberline {8}{\ignorespaces Upper bounds on the cost of ${\sf  Vm}$ instructions}}{16}{table.8}}
    93 \newlabel{cost-approx-instr}{{8}{16}{Upper bounds on the cost of $\vm $ instructions\relax }{table.8}{}}
    94 \newlabel{annot-vm-mips}{{7}{16}{$\mips $ and $\vm $ cost annotations\relax }{theorem.7}{}}
    95 \newlabel{labelled-simulation-vm-mips}{{8}{16}{$\mips $ and $\vm $ cost annotations\relax }{theorem.8}{}}
    96 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2}${\sf  Imp}$ cost annotation}{16}{subsection.3.2}}
    97 \newlabel{imp-cost-annotation}{{3.2}{16}{$\imp $ cost annotation\relax }{subsection.3.2}{}}
    98 \citation{Leroy09-ln}
    99 \@writefile{lot}{\contentsline {table}{\numberline {9}{\ignorespaces Annotation for ${\sf  Imp}$ programs}}{17}{table.9}}
    100 \newlabel{annotation-imp}{{9}{17}{Annotation for $\imp $ programs\relax }{table.9}{}}
    101 \newlabel{annot-imp-vm}{{9}{17}{$\imp $ cost annotation\relax }{theorem.9}{}}
    102 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Composition}{17}{subsection.3.3}}
    103 \newlabel{annot-composition}{{10}{17}{Composition\relax }{theorem.10}{}}
    104 \@writefile{toc}{\contentsline {subsection}{\numberline {3.4}${\sf  Coq}$ development}{18}{subsection.3.4}}
    105 \newlabel{coq-development-sec}{{3.4}{18}{$\coq $ development\relax }{subsection.3.4}{}}
    106 \@writefile{toc}{\contentsline {subsection}{\numberline {3.5}Limitations of the direct approach}{18}{subsection.3.5}}
    107 \newlabel{limitations-direct-sec}{{3.5}{18}{Limitations of the direct approach\relax }{subsection.3.5}{}}
    108 \@writefile{toc}{\contentsline {section}{\numberline {4}Labelling approach for the toy compiler}{18}{section.4}}
    109 \newlabel{label-toy-sec}{{4}{18}{Labelling approach for the toy compiler\relax }{section.4}{}}
    110 \@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Labelled ${\sf  Imp}$}{18}{subsection.4.1}}
    111 \@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Labelled ${\sf  Vm}$}{19}{subsection.4.2}}
    112 \newlabel{labelled-sim-imp-vm}{{11}{19}{Labelled $\vm $\relax }{theorem.11}{}}
    113 \@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Labelled ${\sf  Mips}$}{20}{subsection.4.3}}
    114 \newlabel{sim-vm-mips-prop}{{13}{20}{Labelled $\mips $\relax }{theorem.13}{}}
    115 \@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Labellings and instrumentations}{20}{subsection.4.4}}
    116 \newlabel{lab-instr-erasure-imp}{{14}{20}{Labellings and instrumentations\relax }{theorem.14}{}}
    117 \newlabel{labelling-def}{{15}{20}{Labellings and instrumentations\relax }{theorem.15}{}}
    118 \newlabel{global-commutation-prop}{{16}{20}{Labellings and instrumentations\relax }{theorem.16}{}}
    119 \newlabel{instrument-to-label-prop}{{17}{21}{Labellings and instrumentations\relax }{theorem.17}{}}
    120 \@writefile{toc}{\contentsline {subsection}{\numberline {4.5}Sound and precise labellings}{21}{subsection.4.5}}
    121 \newlabel{sound-label-sec}{{4.5}{21}{Sound and precise labellings\relax }{subsection.4.5}{}}
    122 \newlabel{sound-label-prop}{{20}{21}{Sound and precise labellings\relax }{theorem.20}{}}
    123 \newlabel{precise-label-prop}{{22}{21}{Sound and precise labellings\relax }{theorem.22}{}}
    124 \newlabel{lab-sound}{{23}{21}{Sound and precise labellings\relax }{theorem.23}{}}
    125 \@writefile{lot}{\contentsline {table}{\numberline {10}{\ignorespaces Two labellings for the ${\sf  Imp}$ language}}{22}{table.10}}
    126 \newlabel{labelling}{{10}{22}{Two labellings for the $\imp $ language\relax }{table.10}{}}
    127 \newlabel{ann-correct}{{25}{22}{Sound and precise labellings\relax }{theorem.25}{}}
    128 \citation{CIL02}
    129 \citation{Leroy09}
    130 \@writefile{toc}{\contentsline {section}{\numberline {5}A ${\sf  C}$ compiler}{23}{section.5}}
    131 \newlabel{C-compiler-sec}{{5}{23}{A $\C $ compiler\relax }{section.5}{}}
    132 \@writefile{toc}{\contentsline {subsection}{\numberline {5.1}${\sf  Clight}$}{23}{subsection.5.1}}
    133 \@writefile{toc}{\contentsline {subsection}{\numberline {5.2}${\sf  Cminor}$}{23}{subsection.5.2}}
    134 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Clight}$ to ${\sf  Cminor}$.}{23}{section*.3}}
    135 \@writefile{toc}{\contentsline {subsection}{\numberline {5.3}${\sf  RTLAbs}$}{23}{subsection.5.3}}
    136 \newlabel{syntax-clight}{{5.1}{24}{$\Clight $\relax }{subsection.5.1}{}}
    137 \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Syntax of the ${\sf  Clight}$ language}}{24}{figure.1}}
    138 \newlabel{syntax-cminor}{{5.2}{25}{$\Cminor $\relax }{subsection.5.2}{}}
    139 \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Syntax of the ${\sf  Cminor}$ language}}{25}{figure.2}}
    140 \@writefile{lot}{\contentsline {table}{\numberline {11}{\ignorespaces Syntax of the ${\sf  RTLAbs}$ language}}{26}{table.11}}
    141 \newlabel{RTLAbs:syntax}{{11}{26}{Syntax of the $\RTLAbs $ language\relax }{table.11}{}}
    142 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{26}{section*.4}}
    143 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  Cminor}$ to ${\sf  RTLAbs}$.}{26}{section*.5}}
    144 \@writefile{lot}{\contentsline {table}{\numberline {12}{\ignorespaces Syntax of the ${\sf  RTL}$ language}}{27}{table.12}}
    145 \newlabel{RTL:syntax}{{12}{27}{Syntax of the $\RTL $ language\relax }{table.12}{}}
    146 \@writefile{toc}{\contentsline {subsection}{\numberline {5.4}${\sf  RTL}$}{27}{subsection.5.4}}
    147 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{27}{section*.6}}
    148 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTLAbs}$ to ${\sf  RTL}$.}{27}{section*.7}}
    149 \@writefile{toc}{\contentsline {subsection}{\numberline {5.5}${\sf  ERTL}$}{27}{subsection.5.5}}
    150 \@writefile{lot}{\contentsline {table}{\numberline {13}{\ignorespaces Syntax of the ${\sf  ERTL}$ language}}{28}{table.13}}
    151 \newlabel{ERTL:syntax}{{13}{28}{Syntax of the $\ERTL $ language\relax }{table.13}{}}
    152 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{28}{section*.8}}
    153 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  RTL}$ to ${\sf  ERTL}$.}{28}{section*.9}}
    154 \@writefile{toc}{\contentsline {paragraph}{Optimizations.}{28}{section*.10}}
    155 \@writefile{lot}{\contentsline {table}{\numberline {14}{\ignorespaces Syntax of the ${\sf  LTL}$ language}}{29}{table.14}}
    156 \newlabel{LTL:syntax}{{14}{29}{Syntax of the $\LTL $ language\relax }{table.14}{}}
    157 \@writefile{toc}{\contentsline {subsection}{\numberline {5.6}${\sf  LTL}$}{29}{subsection.5.6}}
    158 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{29}{section*.11}}
    159 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  ERTL}$ to ${\sf  LTL}$.}{29}{section*.12}}
    160 \@writefile{toc}{\contentsline {paragraph}{Optimizations.}{29}{section*.13}}
    161 \@writefile{lot}{\contentsline {table}{\numberline {15}{\ignorespaces Syntax of the ${\sf  LIN}$ language}}{30}{table.15}}
    162 \newlabel{LIN:syntax}{{15}{30}{Syntax of the $\LIN $ language\relax }{table.15}{}}
    163 \@writefile{toc}{\contentsline {subsection}{\numberline {5.7}${\sf  LIN}$}{30}{subsection.5.7}}
    164 \@writefile{toc}{\contentsline {paragraph}{Syntax.}{30}{section*.14}}
    165 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LTL}$ to ${\sf  LIN}$.}{30}{section*.15}}
    166 \@writefile{toc}{\contentsline {subsection}{\numberline {5.8}${\sf  Mips}$}{30}{subsection.5.8}}
    167 \@writefile{toc}{\contentsline {paragraph}{Translation of ${\sf  LIN}$ to ${\sf  Mips}$.}{30}{section*.16}}
    168 \@writefile{lot}{\contentsline {table}{\numberline {16}{\ignorespaces Syntax of the ${\sf  Mips}$ language}}{31}{table.16}}
    169 \newlabel{mips:syntax}{{16}{31}{Syntax of the $\mips $ language\relax }{table.16}{}}
    170 \@writefile{lot}{\contentsline {table}{\numberline {17}{\ignorespaces Building the annotation of a ${\sf  Clight}$ program in the labelling approach}}{31}{table.17}}
    171 \newlabel{annot-clight-summary}{{17}{31}{Building the annotation of a $\Clight $ program in the labelling approach\relax }{table.17}{}}
    172 \@writefile{toc}{\contentsline {section}{\numberline {6}Labelling approach for the ${\sf  C}$ compiler}{31}{section.6}}
    173 \newlabel{C-label-sec}{{6}{31}{Labelling approach for the $\C $ compiler\relax }{section.6}{}}
    174 \@writefile{toc}{\contentsline {subsection}{\numberline {6.1}Labelled ${\sf  Clight}$ and labelled ${\sf  Cminor}$}{31}{subsection.6.1}}
    175 \@writefile{toc}{\contentsline {subsection}{\numberline {6.2}Labels in ${\sf  RTLAbs}$ and the back-end languages}{32}{subsection.6.2}}
    176 \@writefile{toc}{\contentsline {subsection}{\numberline {6.3}Labelling of the source language}{32}{subsection.6.3}}
    177 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.1}Sequential instructions}{32}{subsubsection.6.3.1}}
    178 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.2}Ternary expressions}{32}{subsubsection.6.3.2}}
    179 \@writefile{toc}{\contentsline {paragraph}{Related cases.}{33}{section*.17}}
    180 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.3}Conditionals}{33}{subsubsection.6.3.3}}
    181 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.4}Loops}{33}{subsubsection.6.3.4}}
    182 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.5}Program Labels and Gotos}{34}{subsubsection.6.3.5}}
    183 \@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.6}Function calls}{34}{subsubsection.6.3.6}}
    184 \newlabel{fun-call-sec}{{6.3.6}{34}{Function calls\relax }{subsubsection.6.3.6}{}}
    185 \@writefile{toc}{\contentsline {subsection}{\numberline {6.4}Verifications on the object code}{35}{subsection.6.4}}
    186 \@writefile{toc}{\contentsline {subsection}{\numberline {6.5}Building the cost annotation}{35}{subsection.6.5}}
    187 \citation{Cerco10}
    188 \bibcite{AbsInt}{1}
    189 \bibcite{Cerco10}{2}
    190 \bibcite{SCADE}{3}
    191 \bibcite{Frama-C}{4}
    192 \bibcite{AbsintScade}{5}
    193 \bibcite{Fornari10}{6}
    194 \bibcite{Larus05}{7}
    195 \@writefile{toc}{\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}}
    196 \@writefile{toc}{\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}}
    197 \newlabel{conclusion-sec}{{7}{36}{Conclusion and future work\relax }{section.7}{}}
    198 \bibcite{Leroy09}{8}
    199 \bibcite{Leroy09-ln}{9}
    200 \bibcite{MP67}{10}
    201 \bibcite{CIL02}{11}
    202 \bibcite{Pottier}{12}
    203 \bibcite{W09}{13}
    204 \@writefile{toc}{\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}}
    205 \@writefile{toc}{\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}}
    206 \newlabel{paper-proofs}{{B}{40}{Proofs\relax }{appendix.B}{}}
    207 \@writefile{toc}{\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}}
    208 \@writefile{toc}{\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref  {soundness-small-step}}{40}{subsection.B.2}}
    209 \newlabel{access-lemma}{{26}{40}{Proof of proposition \ref {soundness-small-step}\relax }{theorem.26}{}}
    210 \@writefile{toc}{\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref  {labelled-simulation-vm-mips}}{41}{subsection.B.3}}
    211 \newlabel{step1}{{7}{41}{Proof of proposition \ref {labelled-simulation-vm-mips}\relax }{equation.B.7}{}}
    212 \@writefile{toc}{\contentsline {paragraph}{The memory realisation.}{41}{section*.19}}
    213 \@writefile{toc}{\contentsline {paragraph}{The inequation.}{41}{section*.20}}
    214 \@writefile{toc}{\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref  {annot-composition}}{41}{subsection.B.4}}
    215 \@writefile{toc}{\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref  {labelled-sim-imp-vm}}{42}{subsection.B.5}}
    216 \@writefile{toc}{\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref  {sim-vm-mips-prop}}{42}{subsection.B.6}}
    217 \@writefile{toc}{\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref  {lab-instr-erasure-imp}}{42}{subsection.B.7}}
    218 \@writefile{toc}{\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref  {global-commutation-prop}}{42}{subsection.B.8}}
    219 \@writefile{toc}{\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref  {instrument-to-label-prop}}{42}{subsection.B.9}}
    220 \@writefile{toc}{\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref  {sound-label-prop}}{43}{subsection.B.10}}
    221 \@writefile{toc}{\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref  {precise-label-prop}}{43}{subsection.B.11}}
    222 \@writefile{toc}{\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref  {lab-sound}}{43}{subsection.B.12}}
    223 \newlabel{precise-lemma}{{29}{43}{Proof of proposition \ref {lab-sound}\relax }{theorem.29}{}}
    224 \@writefile{toc}{\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref  {ann-correct}}{43}{subsection.B.13}}
     28\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{4}{section.1}}
     29\newlabel{intro-sec}{{1}{4}{Introduction\relax }{section.1}{}}
     30\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Meaning of cost annotations}{4}{subsection.1.1}}
  • Deliverables/D2.1/report.log

    r1694 r1982  
    1 This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2011.12.11)  26 JAN 2012 18:29
     1This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=latex 2010.10.5)  11 MAR 2011 18:13
    22entering extended mode
    33 %&-line parsing enabled.
    4 **report.tex
     4**report
    55(./report.tex
    66LaTeX2e <2009/09/24>
     
    4444
    4545(/usr/share/texmf-texlive/tex/latex/pdftex-def/pdftex.def
    46 File: pdftex.def 2010/03/12 v0.04p Graphics/color for pdfTeX
     46File: pdftex.def 2009/08/25 v0.04m Graphics/color for pdfTeX
     47
     48
     49! Package pdftex.def Error: PDF mode expected, but DVI mode detected!
     50(pdftex.def)                If you are using `latex', then call `pdflatex'.
     51(pdftex.def)                Otherwise check and correct the driver options.
     52(pdftex.def)                Error recovery by switching to PDF mode.
     53
     54See the pdftex.def package documentation for explanation.
     55Type  H <return>  for immediate help.
     56 ...                                             
     57                                                 
     58l.385     }\@ehc
     59               
     60?
    4761\Gread@gobject=\count87
    4862))
    4963\Gin@req@height=\dimen103
    5064\Gin@req@width=\dimen104
    51 )
    52 (/usr/share/texmf-texlive/tex/latex/base/latexsym.sty
     65) (/usr/share/texmf-texlive/tex/latex/base/latexsym.sty
    5366Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
    5467\symlasy=\mathgroup4
     
    275288Package: xspace 2006/05/08 v1.12 Space after command names (DPC,MH)
    276289)
    277 (/usr/share/texmf-texlive/tex/generic/xypic/xy.sty
    278 (/usr/share/texmf-texlive/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes,
    279 docmode, (/usr/share/texmf-texlive/tex/generic/xypic/xyrecat.tex)
    280 (/usr/share/texmf-texlive/tex/generic/xypic/xyidioms.tex)
    281 
    282  Xy-pic version 3.7 <1999/02/16>
    283  Copyright (c) 1991-1998 by Kristoffer H. Rose <krisrose@ens-lyon.fr>
    284  Xy-pic is free software: see the User's Guide for details.
    285 
    286 Loading kernel: messages; fonts; allocations: state,
    287 \X@c=\dimen118
    288 \Y@c=\dimen119
    289 \U@c=\dimen120
    290 \D@c=\dimen121
    291 \L@c=\dimen122
    292 \R@c=\dimen123
    293 \Edge@c=\toks24
    294 \X@p=\dimen124
    295 \Y@p=\dimen125
    296 \U@p=\dimen126
    297 \D@p=\dimen127
    298 \L@p=\dimen128
    299 \R@p=\dimen129
    300 \Edge@p=\toks25
    301 \X@origin=\dimen130
    302 \Y@origin=\dimen131
    303 \X@xbase=\dimen132
    304 \Y@xbase=\dimen133
    305 \X@ybase=\dimen134
    306 \Y@ybase=\dimen135
    307 \X@min=\dimen136
    308 \Y@min=\dimen137
    309 \X@max=\dimen138
    310 \Y@max=\dimen139
    311 \lastobjectbox@=\box28
    312 \zerodotbox@=\box29
    313 \almostz@=\dimen140
    314  direction,
    315 \d@X=\dimen141
    316 \d@Y=\dimen142
    317 \K@=\count108
    318 \KK@=\count109
    319 \Direction=\count110
    320 \K@dXdY=\dimen143
    321 \K@dYdX=\dimen144
    322 \xyread@=\read1
    323 \xywrite@=\write3
    324 \csp@=\count111
    325 \quotPTK@=\dimen145
    326 
    327 utility macros; pictures: \xy, positions,
    328 \swaptoks@@=\toks26
    329 \connectobjectbox@@=\box30
    330  objects,
    331 \styletoks@=\toks27
    332  decorations;
    333 kernel objects: directionals, circles, text; options; algorithms: directions,
    334 edges, connections;  Xy-pic loaded)
    335 Package: xy 1999/02/16 Xy-pic version 3.7
    336 
    337 (/usr/share/texmf-texlive/tex/generic/xypic/xyall.tex
    338  Xy-pic option: All features v.3.3
    339 (/usr/share/texmf-texlive/tex/generic/xypic/xycurve.tex
    340  Xy-pic option: Curve and Spline extension v.3.7 curve,
    341 \crv@cnt@=\count112
    342 \crvpts@=\toks28
    343 \splinebox@=\box31
    344 \splineval@=\dimen146
    345 \splinedepth@=\dimen147
    346 \splinetol@=\dimen148
    347 \splinelength@=\dimen149
    348  circles,
    349 \L@=\dimen150
    350  loaded)
    351 (/usr/share/texmf-texlive/tex/generic/xypic/xyframe.tex
    352  Xy-pic option: Frame and Bracket extension v.3.7 loaded)
    353 (/usr/share/texmf-texlive/tex/generic/xypic/xycmtip.tex
    354  Xy-pic option: Computer Modern tip extension v.3.3
    355 (/usr/share/texmf-texlive/tex/generic/xypic/xytips.tex
    356  Xy-pic option: More Tips extension v.3.3 loaded) loaded)
    357 (/usr/share/texmf-texlive/tex/generic/xypic/xyline.tex
    358  Xy-pic option: Line styles extension v.3.6
    359 \xylinethick@=\dimen151
    360  loaded)
    361 (/usr/share/texmf-texlive/tex/generic/xypic/xyrotate.tex
    362  Xy-pic option: Rotate and Scale extension v.3.3 loaded)
    363 (/usr/share/texmf-texlive/tex/generic/xypic/xycolor.tex
    364  Xy-pic option: Colour extension v.3.3 loaded)
    365 (/usr/share/texmf-texlive/tex/generic/xypic/xymatrix.tex
    366  Xy-pic option: Matrix feature v.3.4
    367 \Row=\count113
    368 \Col=\count114
    369 \queue@=\toks29
    370 \queue@@=\toks30
    371 \qcount@=\count115
    372 \qcount@@=\count116
    373 \matrixsize@=\count117
    374  loaded)
    375 (/usr/share/texmf-texlive/tex/generic/xypic/xyarrow.tex
    376  Xy-pic option: Arrow and Path feature v.3.5 path, \ar, loaded)
    377 (/usr/share/texmf-texlive/tex/generic/xypic/xygraph.tex
    378  Xy-pic option: Graph feature v.3.7 loaded) loaded))
     290
     291! LaTeX Error: File `xy.sty' not found.
     292
     293Type X to quit or <RETURN> to proceed,
     294or enter new name. (Default extension: sty)
     295
     296Enter file name:
     297
     298! LaTeX Error: Unknown option `all' for package `xy'.
     299
     300See the LaTeX manual or LaTeX Companion for explanation.
     301Type  H <return>  for immediate help.
     302 ...                                             
     303                                                 
     304l.32 \usepackage
     305                {graphics,color}
     306?
    379307(/usr/share/texmf-texlive/tex/latex/graphics/color.sty
    380308Package: color 2005/11/14 v1.0j Standard LaTeX Color (DPC)
     
    387315(/usr/share/texmf-texlive/tex/latex/tools/array.sty
    388316Package: array 2008/09/09 v2.4c Tabular extension package (FMi)
    389 \col@sep=\dimen152
    390 \extrarowheight=\dimen153
    391 \NC@list=\toks31
     317\col@sep=\dimen118
     318\extrarowheight=\dimen119
     319\NC@list=\toks24
    392320\extratabsurround=\skip46
    393321\backup@length=\skip47
    394322)
    395 \c@theorem=\count118
     323\c@theorem=\count108
    396324
    397325
     
    418346 (/usr/share/texmf-texlive/tex/context/base/supp-pdf.mkii
    419347[Loading MPS to PDF converter (version 2006.09.02).]
    420 \scratchcounter=\count119
    421 \scratchdimen=\dimen154
    422 \scratchbox=\box32
    423 \nofMPsegments=\count120
    424 \nofMParguments=\count121
    425 \everyMPshowfont=\toks32
    426 \MPscratchCnt=\count122
    427 \MPscratchDim=\dimen155
    428 \MPnumerator=\count123
    429 \everyMPtoPDFconversion=\toks33
     348\scratchcounter=\count109
     349\scratchdimen=\dimen120
     350\scratchbox=\box28
     351\nofMPsegments=\count110
     352\nofMParguments=\count111
     353\everyMPshowfont=\toks25
     354\MPscratchCnt=\count112
     355\MPscratchDim=\dimen121
     356\MPnumerator=\count113
     357\everyMPtoPDFconversion=\toks26
    430358)
    431359Package hyperref Info: Link coloring ON on input line 538.
     
    436364Package: refcount 2008/08/11 v3.1 Data extraction from references (HO)
    437365)
    438 \c@section@level=\count124
     366\c@section@level=\count114
    439367)
    440368LaTeX Info: Redefining \ref on input line 538.
     
    442370 (./report.out)
    443371(./report.out)
    444 \@outlinefile=\write4
    445 \openout4 = `report.out'.
    446 
    447 \AtBeginShipoutBox=\box33
    448  <../style/cerco_logo.png, id=283, 804.00375pt x 213.79875pt>
     372\@outlinefile=\write3
     373\openout3 = `report.out'.
     374
     375\AtBeginShipoutBox=\box29
     376 <../style/cerco_logo.png, id=3, 804.00375pt x 213.79875pt>
    449377File: ../style/cerco_logo.png Graphic file (type png)
    450378
     
    477405[2
    478406
    479 ] (./report.toc [3])
    480 \tf@toc=\write5
    481 \openout5 = `report.toc'.
    482 
    483  [4] (./text.tex
     407]
     408
     409Package hyperref Warning: old toc file detected, not used; run LaTeX again.
     410
     411\tf@toc=\write4
     412\openout4 = `report.toc'.
     413
     414[3] (./text.tex
     415
     416LaTeX Warning: Citation `Leroy09' on page 4 undefined on input line 9.
     417
     418
     419LaTeX Warning: Citation `Cerco10' on page 4 undefined on input line 11.
     420
     421
     422LaTeX Warning: Citation `SCADE' on page 4 undefined on input line 22.
     423
     424
     425LaTeX Warning: Citation `Fornari10' on page 4 undefined on input line 22.
     426
     427
     428LaTeX Warning: Citation `AbsInt' on page 4 undefined on input line 24.
     429
     430
     431LaTeX Warning: Citation `AbsintScade' on page 4 undefined on input line 24.
     432
     433
     434LaTeX Warning: Citation `W09' on page 4 undefined on input line 28.
     435
     436
     437LaTeX Warning: Citation `Frama-C' on page 4 undefined on input line 34.
     438
    484439LaTeX Font Info:    Try loading font information for OMS+cmr on input line 54.
    485 
    486440(/usr/share/texmf-texlive/tex/latex/base/omscmr.fd
    487441File: omscmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
     
    489443LaTeX Font Info:    Font shape `OMS/cmr/m/n' in size <10.95> not available
    490444(Font)              Font shape `OMS/cmsy/m/n' tried instead on input line 54.
    491  [5] <xymatrix 4x2 239>
    492 [6] <xymatrix 4x3 421>
    493 Overfull \hbox (3.0225pt too wide) detected at line 219
    494 []
    495  []
    496 
    497 [7] <xymatrix 3x1 96> [8] [9] [10]
    498 
    499 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    500 (hyperref)                removing `math shift' on input line 676.
    501 
    502 
    503 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    504 (hyperref)                removing `math shift' on input line 676.
    505 
    506 
    507 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    508 (hyperref)                removing `math shift' on input line 676.
    509 
    510 
    511 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    512 (hyperref)                removing `math shift' on input line 676.
    513 
    514 [11] [12]
    515 
    516 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    517 (hyperref)                removing `math shift' on input line 843.
    518 
    519 
    520 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    521 (hyperref)                removing `math shift' on input line 843.
    522 
    523 
    524 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    525 (hyperref)                removing `math shift' on input line 910.
    526 
    527 
    528 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    529 (hyperref)                removing `math shift' on input line 910.
    530 
    531 
    532 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    533 (hyperref)                removing `math shift' on input line 910.
    534 
    535 
    536 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    537 (hyperref)                removing `math shift' on input line 910.
    538 
    539 [13] <xymatrix 3x2 231> [14]
    540 
    541 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    542 (hyperref)                removing `math shift' on input line 1057.
    543 
    544 
    545 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    546 (hyperref)                removing `math shift' on input line 1057.
    547 
    548 
    549 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    550 (hyperref)                removing `math shift' on input line 1057.
    551 
    552 
    553 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    554 (hyperref)                removing `math shift' on input line 1057.
    555 
    556 [15]
    557 
    558 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    559 (hyperref)                removing `math shift' on input line 1198.
    560 
    561 
    562 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    563 (hyperref)                removing `math shift' on input line 1198.
    564 
    565 [16]
    566 
    567 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    568 (hyperref)                removing `math shift' on input line 1329.
    569 
    570 
    571 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    572 (hyperref)                removing `math shift' on input line 1329.
    573 
    574 [17]
    575 
    576 Package array Warning: Column M is already defined on input line 1383.
    577 
    578 <xymatrix 3x3 413>
    579 Overfull \hbox (15.98283pt too wide) detected at line 1423
    580 []
    581  []
    582 
    583 
    584 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    585 (hyperref)                removing `math shift' on input line 1429.
    586 
    587 
    588 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    589 (hyperref)                removing `math shift' on input line 1429.
    590 
    591 [18]
    592 
    593 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    594 (hyperref)                removing `math shift' on input line 1512.
    595 
    596 
    597 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    598 (hyperref)                removing `math shift' on input line 1512.
    599 
    600 [19]
    601 
    602 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    603 (hyperref)                removing `math shift' on input line 1574.
    604 
    605 
    606 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    607 (hyperref)                removing `math shift' on input line 1574.
    608 
    609 
    610 Overfull \hbox (6.32399pt too wide) in paragraph at lines 1651--1655
    611 []\OT1/cmr/m/it/10.95 Let $\OML/cmm/m/it/10.95 S$ \OT1/cmr/m/it/10.95 be an $[]
    612 []$ com-mand. If $\OT1/cmr/m/n/10.95 (\OMS/cmsy/m/n/10.95 I\OT1/cmr/m/n/10.95 (
    613 \OML/cmm/m/it/10.95 S\OT1/cmr/m/n/10.95 )\OML/cmm/m/it/10.95 ; s\OT1/cmr/m/n/10
    614 .95 [\OML/cmm/m/it/10.95 c=[]\OT1/cmr/m/n/10.95 ]) \OMS/cmsy/m/n/10.95 + \OML/c
    615 mm/m/it/10.95 s[]\OT1/cmr/m/n/10.95 [\OML/cmm/m/it/10.95 c \OT1/cmr/m/n/10.95 +
    616  \OML/cmm/m/it/10.95 ^^N=[]\OT1/cmr/m/n/10.95 ]$ \OT1/cmr/m/it/10.95 then $\OMS
    617 /cmsy/m/n/10.95 9 \OML/cmm/m/it/10.95 ^^U  ^^T\OT1/cmr/m/n/10.95 (\OML/cmm/m/it
    618 /10.95 ^^U\OT1/cmr/m/n/10.95 ) =
    619  []
    620 
    621 [20] [21]
    622 
    623 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    624 (hyperref)                removing `math shift' on input line 1889.
    625 
    626 
    627 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    628 (hyperref)                removing `math shift' on input line 1889.
    629 
    630 [22]
    631 
    632 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    633 (hyperref)                removing `math shift' on input line 1895.
    634 
    635 
    636 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    637 (hyperref)                removing `math shift' on input line 1895.
    638 
    639 
    640 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    641 (hyperref)                removing `math shift' on input line 1962.
    642 
    643 
    644 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    645 (hyperref)                removing `math shift' on input line 1962.
    646 
    647 
    648 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    649 (hyperref)                removing `math shift' on input line 2019.
    650 
    651 
    652 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    653 (hyperref)                removing `math shift' on input line 2019.
    654 
    655 [23] [24] [25]
    656 
    657 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    658 (hyperref)                removing `math shift' on input line 2145.
    659 
    660 
    661 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    662 (hyperref)                removing `math shift' on input line 2145.
    663 
    664 [26]
    665 
    666 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    667 (hyperref)                removing `math shift' on input line 2237.
    668 
    669 
    670 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    671 (hyperref)                removing `math shift' on input line 2237.
    672 
    673 [27] [28]
    674 
    675 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    676 (hyperref)                removing `math shift' on input line 2349.
    677 
    678 
    679 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    680 (hyperref)                removing `math shift' on input line 2349.
    681 
    682 
    683 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    684 (hyperref)                removing `math shift' on input line 2433.
    685 
    686 
    687 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    688 (hyperref)                removing `math shift' on input line 2433.
    689 
    690 [29]
    691 
    692 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    693 (hyperref)                removing `math shift' on input line 2502.
    694 
    695 
    696 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    697 (hyperref)                removing `math shift' on input line 2502.
    698 
    699 
    700 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    701 (hyperref)                removing `math shift' on input line 2566.
    702 
    703 
    704 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    705 (hyperref)                removing `math shift' on input line 2566.
    706 
    707 [30]
    708 Underfull \hbox (badness 10000) in paragraph at lines 2580--2581
    709 
    710  []
    711 
    712 
    713 Underfull \hbox (badness 10000) in paragraph at lines 2582--2584
    714 
    715  []
    716 
    717 
    718 Underfull \hbox (badness 10000) in paragraph at lines 2585--2589
    719 
    720  []
    721 
    722 
    723 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    724 (hyperref)                removing `math shift' on input line 2601.
    725 
    726 
    727 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    728 (hyperref)                removing `math shift' on input line 2601.
    729 
    730 
    731 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    732 (hyperref)                removing `math shift' on input line 2601.
    733 
    734 
    735 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    736 (hyperref)                removing `math shift' on input line 2601.
    737 
    738 [31]
    739 
    740 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    741 (hyperref)                removing `math shift' on input line 2615.
    742 
    743 
    744 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    745 (hyperref)                removing `math shift' on input line 2615.
    746 
    747 [32]
    748 LaTeX Font Info:    Try loading font information for OMS+cmtt on input line 271
    749 9.
    750 LaTeX Font Info:    No file OMScmtt.fd. on input line 2719.
    751 
    752 
    753 LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
    754 (Font)              using `OMS/cmsy/m/n' instead
    755 (Font)              for symbol `textbraceleft' on input line 2719.
    756 
    757 [33] [34] [35]
    758 Underfull \hbox (badness 10000) in paragraph at lines 2979--2983
    759 []\OT1/cmr/m/n/9 Certified Com-plex-ity (Project de-scrip-tion).  ICT-2007.8.0
    760 FET Open, Grant 243881.
    761  []
    762 
    763 [36]
    764 Underfull \hbox (badness 10000) in paragraph at lines 3037--3040
    765 []\OT1/cmr/m/n/9 F. Pot-tier.  Com-pi-la-tion (INF 564), []Ecole Poly-tech-niqu
    766 e, 2009-2010.
    767  []
    768 
    769 [37]
    770 
    771 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    772 (hyperref)                removing `math shift' on input line 3053.
    773 
    774 
    775 Package hyperref Warning: Token not allowed in a PDF string (PDFDocEncoding):
    776 (hyperref)                removing `math shift' on input line 3053.
    777 
    778 [38] [39] [40] [41] [42]) [43] (./report.aux)
    779 
    780 LaTeX Font Warning: Some font shapes were not available, defaults substituted.
    781 
    782  )
     445 [4]
     446! Undefined control sequence.
     447l.122 \xymatrix
     448               {
     449?
     450! Undefined control sequence.
     451l.124   L_1 \ar
     452               [d]^{An_1} \ar[r]^{\cl{C}_1}
     453?
     454! Undefined control sequence.
     455l.124   L_1 \ar[d]^{An_1} \ar
     456                             [r]^{\cl{C}_1}
     457?
     458! Misplaced alignment tab character &.
     459l.125 &
     460        L_2 \ar[d]^{An_1}
     461?
     462! Undefined control sequence.
     463l.125 & L_2 \ar
     464               [d]^{An_1}
     465?
     466! Emergency stop.
     467l.125 & L_2 \ar
     468               [d]^{An_1}
     469End of file on the terminal!
     470
     471 
    783472Here is how much of TeX's memory you used:
    784  8519 strings out of 495021
    785  110821 string characters out of 1180925
    786  247727 words of memory out of 3000000
    787  11300 multiletter control sequences out of 15000+50000
    788  28130 words of font info for 114 fonts, out of 3000000 for 9000
     473 5860 strings out of 495062
     474 78817 string characters out of 1182644
     475 155725 words of memory out of 3000000
     476 8910 multiletter control sequences out of 15000+50000
     477 14988 words of font info for 57 fonts, out of 3000000 for 9000
    789478 28 hyphenation exceptions out of 8191
    790  45i,22n,39p,274b,821s stack positions out of 5000i,500n,10000p,200000b,50000s
    791 </usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/sha
    792 re/texmf-texlive/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texmf-te
    793 xlive/fonts/type1/public/amsfonts/cm/cmbx6.pfb></usr/share/texmf-texlive/fonts/
    794 type1/public/amsfonts/cm/cmbx8.pfb></usr/share/texmf-texlive/fonts/type1/public
    795 /amsfonts/cm/cmbx9.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm
    796 /cmcsc10.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmex10.pf
    797 b></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cmextra/cmex9.pfb></usr
    798 /share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texm
    799 f-texlive/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/texmf-texlive/f
    800 onts/type1/public/amsfonts/cm/cmmi5.pfb></usr/share/texmf-texlive/fonts/type1/p
    801 ublic/amsfonts/cm/cmmi6.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfon
    802 ts/cm/cmmi8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmmi9.
    803 pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/sh
    804 are/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texmf-te
    805 xlive/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texmf-texlive/fonts/
    806 type1/public/amsfonts/cm/cmr5.pfb></usr/share/texmf-texlive/fonts/type1/public/
    807 amsfonts/cm/cmr6.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/c
    808 mr8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr
    809 /share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr/share/texm
    810 f-texlive/fonts/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texmf-texlive/f
    811 onts/type1/public/amsfonts/cm/cmss12.pfb></usr/share/texmf-texlive/fonts/type1/
    812 public/amsfonts/cm/cmss8.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfo
    813 nts/cm/cmss9.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy1
    814 0.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy5.pfb></usr/
    815 share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmsy6.pfb></usr/share/texmf-
    816 texlive/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texmf-texlive/font
    817 s/type1/public/amsfonts/cm/cmsy9.pfb></usr/share/texmf-texlive/fonts/type1/publ
    818 ic/amsfonts/cm/cmti10.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts
    819 /cm/cmti7.pfb></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmti8.pf
    820 b></usr/share/texmf-texlive/fonts/type1/public/amsfonts/cm/cmti9.pfb></usr/shar
    821 e/texmf-texlive/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texmf-tex
    822 live/fonts/type1/public/amsfonts/cm/cmtt9.pfb></usr/share/texmf-texlive/fonts/t
    823 ype1/public/amsfonts/latxfont/lasy10.pfb></usr/share/texmf-texlive/fonts/type1/
    824 public/amsfonts/latxfont/lasy9.pfb></usr/share/texmf-texlive/fonts/type1/public
    825 /xypic/xyatip10.pfb></usr/share/texmf-texlive/fonts/type1/public/xypic/xybtip10
    826 .pfb>
    827 Output written on report.pdf (43 pages, 868174 bytes).
    828 PDF statistics:
    829  960 PDF objects out of 1000 (max. 8388607)
    830  211 named destinations out of 1000 (max. 500000)
    831  566 words of extra memory for PDF output out of 10000 (max. 10000000)
    832 
     479 45i,6n,38p,248b,310s stack positions out of 5000i,500n,10000p,200000b,50000s
     480!  ==> Fatal error occurred, no output PDF file produced!
  • Deliverables/D2.1/report.out

    r59 r1982  
    11\BOOKMARK [1][]{section.1}{Introduction}{}
    22\BOOKMARK [2][]{subsection.1.1}{Meaning of cost annotations}{section.1}
    3 \BOOKMARK [2][]{subsection.1.2}{Soundness and precision of cost annotations}{section.1}
    4 \BOOKMARK [2][]{subsection.1.3}{Compositionality}{section.1}
    5 \BOOKMARK [2][]{subsection.1.4}{Direct approach to cost annotations}{section.1}
    6 \BOOKMARK [2][]{subsection.1.5}{Labelling approach to cost annotations}{section.1}
    7 \BOOKMARK [2][]{subsection.1.6}{A toy compiler}{section.1}
    8 \BOOKMARK [2][]{subsection.1.7}{A C compiler}{section.1}
    9 \BOOKMARK [2][]{subsection.1.8}{Organisation}{section.1}
    10 \BOOKMARK [1][]{section.2}{A toy compiler}{}
    11 \BOOKMARK [2][]{subsection.2.1}{Imp: language and semantics}{section.2}
    12 \BOOKMARK [2][]{subsection.2.2}{Big-step semantics}{section.2}
    13 \BOOKMARK [2][]{subsection.2.3}{Small-step semantics}{section.2}
    14 \BOOKMARK [2][]{subsection.2.4}{Vm: language and semantics}{section.2}
    15 \BOOKMARK [2][]{subsection.2.5}{Compilation from Imp to Vm}{section.2}
    16 \BOOKMARK [2][]{subsection.2.6}{Soundness of compilation for the big-step semantics}{section.2}
    17 \BOOKMARK [2][]{subsection.2.7}{Soundness of compilation for the small-step semantics}{section.2}
    18 \BOOKMARK [2][]{subsection.2.8}{Compiled code is well-formed}{section.2}
    19 \BOOKMARK [2][]{subsection.2.9}{Mips: language and semantics}{section.2}
    20 \BOOKMARK [2][]{subsection.2.10}{Compilation from Vm to Mips}{section.2}
    21 \BOOKMARK [1][]{section.3}{Direct approach for the toy compiler}{}
    22 \BOOKMARK [2][]{subsection.3.1}{Mips and Vm cost annotations}{section.3}
    23 \BOOKMARK [2][]{subsection.3.2}{Imp cost annotation}{section.3}
    24 \BOOKMARK [2][]{subsection.3.3}{Composition}{section.3}
    25 \BOOKMARK [2][]{subsection.3.4}{Coq development}{section.3}
    26 \BOOKMARK [2][]{subsection.3.5}{Limitations of the direct approach}{section.3}
    27 \BOOKMARK [1][]{section.4}{Labelling approach for the toy compiler}{}
    28 \BOOKMARK [2][]{subsection.4.1}{Labelled Imp}{section.4}
    29 \BOOKMARK [2][]{subsection.4.2}{Labelled Vm}{section.4}
    30 \BOOKMARK [2][]{subsection.4.3}{Labelled Mips}{section.4}
    31 \BOOKMARK [2][]{subsection.4.4}{Labellings and instrumentations}{section.4}
    32 \BOOKMARK [2][]{subsection.4.5}{Sound and precise labellings}{section.4}
    33 \BOOKMARK [1][]{section.5}{A C compiler}{}
    34 \BOOKMARK [2][]{subsection.5.1}{Clight}{section.5}
    35 \BOOKMARK [2][]{subsection.5.2}{Cminor}{section.5}
    36 \BOOKMARK [2][]{subsection.5.3}{RTLAbs}{section.5}
    37 \BOOKMARK [2][]{subsection.5.4}{RTL}{section.5}
    38 \BOOKMARK [2][]{subsection.5.5}{ERTL}{section.5}
    39 \BOOKMARK [2][]{subsection.5.6}{LTL}{section.5}
    40 \BOOKMARK [2][]{subsection.5.7}{LIN}{section.5}
    41 \BOOKMARK [2][]{subsection.5.8}{Mips}{section.5}
    42 \BOOKMARK [1][]{section.6}{Labelling approach for the C compiler}{}
    43 \BOOKMARK [2][]{subsection.6.1}{Labelled Clight and labelled Cminor}{section.6}
    44 \BOOKMARK [2][]{subsection.6.2}{Labels in RTLAbs and the back-end languages}{section.6}
    45 \BOOKMARK [2][]{subsection.6.3}{Labelling of the source language}{section.6}
    46 \BOOKMARK [3][]{subsubsection.6.3.1}{Sequential instructions}{subsection.6.3}
    47 \BOOKMARK [3][]{subsubsection.6.3.2}{Ternary expressions}{subsection.6.3}
    48 \BOOKMARK [3][]{subsubsection.6.3.3}{Conditionals}{subsection.6.3}
    49 \BOOKMARK [3][]{subsubsection.6.3.4}{Loops}{subsection.6.3}
    50 \BOOKMARK [3][]{subsubsection.6.3.5}{Program Labels and Gotos}{subsection.6.3}
    51 \BOOKMARK [3][]{subsubsection.6.3.6}{Function calls}{subsection.6.3}
    52 \BOOKMARK [2][]{subsection.6.4}{Verifications on the object code}{section.6}
    53 \BOOKMARK [2][]{subsection.6.5}{Building the cost annotation}{section.6}
    54 \BOOKMARK [2][]{subsection.6.6}{Testing}{section.6}
    55 \BOOKMARK [1][]{section.7}{Conclusion and future work}{}
    56 \BOOKMARK [1][]{appendix.A}{Assessment of the deliverable within the CerCo project}{}
    57 \BOOKMARK [1][]{appendix.B}{Proofs}{}
    58 \BOOKMARK [2][]{subsection.B.1}{Notation}{appendix.B}
    59 \BOOKMARK [2][]{subsection.B.2}{Proof of proposition 4}{appendix.B}
    60 \BOOKMARK [2][]{subsection.B.3}{Proof of proposition 8}{appendix.B}
    61 \BOOKMARK [2][]{subsection.B.4}{Proof of proposition 10}{appendix.B}
    62 \BOOKMARK [2][]{subsection.B.5}{Proof of proposition 11}{appendix.B}
    63 \BOOKMARK [2][]{subsection.B.6}{Proof of proposition 13}{appendix.B}
    64 \BOOKMARK [2][]{subsection.B.7}{Proof of proposition 14}{appendix.B}
    65 \BOOKMARK [2][]{subsection.B.8}{Proof of proposition 16}{appendix.B}
    66 \BOOKMARK [2][]{subsection.B.9}{Proof of proposition 17}{appendix.B}
    67 \BOOKMARK [2][]{subsection.B.10}{Proof of proposition 20}{appendix.B}
    68 \BOOKMARK [2][]{subsection.B.11}{Proof of proposition 22}{appendix.B}
    69 \BOOKMARK [2][]{subsection.B.12}{Proof of proposition 23}{appendix.B}
    70 \BOOKMARK [2][]{subsection.B.13}{Proof of proposition 25}{appendix.B}
  • Deliverables/D2.1/report.toc

    r59 r1982  
    1 \select@language {english}
    2 \contentsline {paragraph}{Abstract}{2}{section*.1}
    3 \contentsline {section}{\numberline {1}Introduction}{5}{section.1}
    4 \contentsline {subsection}{\numberline {1.1}Meaning of cost annotations}{5}{subsection.1.1}
    5 \contentsline {subsection}{\numberline {1.2}Soundness and precision of cost annotations}{6}{subsection.1.2}
    6 \contentsline {subsection}{\numberline {1.3}Compositionality}{6}{subsection.1.3}
    7 \contentsline {subsection}{\numberline {1.4}Direct approach to cost annotations}{6}{subsection.1.4}
    8 \contentsline {subsection}{\numberline {1.5}Labelling approach to cost annotations}{7}{subsection.1.5}
    9 \contentsline {subsection}{\numberline {1.6}A toy compiler}{8}{subsection.1.6}
    10 \contentsline {subsection}{\numberline {1.7}A C compiler}{8}{subsection.1.7}
    11 \contentsline {subsection}{\numberline {1.8}Organisation}{9}{subsection.1.8}
    12 \contentsline {section}{\numberline {2}A toy compiler}{9}{section.2}
    13 \contentsline {subsection}{\numberline {2.1}{\sf Imp}: language and semantics}{9}{subsection.2.1}
    14 \contentsline {subsection}{\numberline {2.2}Big-step semantics}{9}{subsection.2.2}
    15 \contentsline {subsection}{\numberline {2.3}Small-step semantics}{10}{subsection.2.3}
    16 \contentsline {subsection}{\numberline {2.4}{\sf Vm}: language and semantics}{11}{subsection.2.4}
    17 \contentsline {subsection}{\numberline {2.5}Compilation from ${\sf Imp}$ to ${\sf Vm}$}{12}{subsection.2.5}
    18 \contentsline {subsection}{\numberline {2.6}Soundness of compilation for the big-step semantics}{12}{subsection.2.6}
    19 \contentsline {subsection}{\numberline {2.7}Soundness of compilation for the small-step semantics}{12}{subsection.2.7}
    20 \contentsline {subsection}{\numberline {2.8}Compiled code is well-formed}{13}{subsection.2.8}
    21 \contentsline {subsection}{\numberline {2.9}${\sf Mips}$: language and semantics}{13}{subsection.2.9}
    22 \contentsline {subsection}{\numberline {2.10}Compilation from ${\sf Vm}$ to ${\sf Mips}$}{14}{subsection.2.10}
    23 \contentsline {section}{\numberline {3}Direct approach for the toy compiler}{14}{section.3}
    24 \contentsline {subsection}{\numberline {3.1}${\sf Mips}$ and ${\sf Vm}$ cost annotations}{15}{subsection.3.1}
    25 \contentsline {subsection}{\numberline {3.2}${\sf Imp}$ cost annotation}{16}{subsection.3.2}
    26 \contentsline {subsection}{\numberline {3.3}Composition}{17}{subsection.3.3}
    27 \contentsline {subsection}{\numberline {3.4}${\sf Coq}$ development}{18}{subsection.3.4}
    28 \contentsline {subsection}{\numberline {3.5}Limitations of the direct approach}{18}{subsection.3.5}
    29 \contentsline {section}{\numberline {4}Labelling approach for the toy compiler}{18}{section.4}
    30 \contentsline {subsection}{\numberline {4.1}Labelled ${\sf Imp}$}{18}{subsection.4.1}
    31 \contentsline {subsection}{\numberline {4.2}Labelled ${\sf Vm}$}{19}{subsection.4.2}
    32 \contentsline {subsection}{\numberline {4.3}Labelled ${\sf Mips}$}{20}{subsection.4.3}
    33 \contentsline {subsection}{\numberline {4.4}Labellings and instrumentations}{20}{subsection.4.4}
    34 \contentsline {subsection}{\numberline {4.5}Sound and precise labellings}{21}{subsection.4.5}
    35 \contentsline {section}{\numberline {5}A ${\sf C}$ compiler}{23}{section.5}
    36 \contentsline {subsection}{\numberline {5.1}${\sf Clight}$}{23}{subsection.5.1}
    37 \contentsline {subsection}{\numberline {5.2}${\sf Cminor}$}{23}{subsection.5.2}
    38 \contentsline {paragraph}{Translation of ${\sf Clight}$ to ${\sf Cminor}$.}{23}{section*.3}
    39 \contentsline {subsection}{\numberline {5.3}${\sf RTLAbs}$}{23}{subsection.5.3}
    40 \contentsline {paragraph}{Syntax.}{26}{section*.4}
    41 \contentsline {paragraph}{Translation of ${\sf Cminor}$ to ${\sf RTLAbs}$.}{26}{section*.5}
    42 \contentsline {subsection}{\numberline {5.4}${\sf RTL}$}{27}{subsection.5.4}
    43 \contentsline {paragraph}{Syntax.}{27}{section*.6}
    44 \contentsline {paragraph}{Translation of ${\sf RTLAbs}$ to ${\sf RTL}$.}{27}{section*.7}
    45 \contentsline {subsection}{\numberline {5.5}${\sf ERTL}$}{27}{subsection.5.5}
    46 \contentsline {paragraph}{Syntax.}{28}{section*.8}
    47 \contentsline {paragraph}{Translation of ${\sf RTL}$ to ${\sf ERTL}$.}{28}{section*.9}
    48 \contentsline {paragraph}{Optimizations.}{28}{section*.10}
    49 \contentsline {subsection}{\numberline {5.6}${\sf LTL}$}{29}{subsection.5.6}
    50 \contentsline {paragraph}{Syntax.}{29}{section*.11}
    51 \contentsline {paragraph}{Translation of ${\sf ERTL}$ to ${\sf LTL}$.}{29}{section*.12}
    52 \contentsline {paragraph}{Optimizations.}{29}{section*.13}
    53 \contentsline {subsection}{\numberline {5.7}${\sf LIN}$}{30}{subsection.5.7}
    54 \contentsline {paragraph}{Syntax.}{30}{section*.14}
    55 \contentsline {paragraph}{Translation of ${\sf LTL}$ to ${\sf LIN}$.}{30}{section*.15}
    56 \contentsline {subsection}{\numberline {5.8}${\sf Mips}$}{30}{subsection.5.8}
    57 \contentsline {paragraph}{Translation of ${\sf LIN}$ to ${\sf Mips}$.}{30}{section*.16}
    58 \contentsline {section}{\numberline {6}Labelling approach for the ${\sf C}$ compiler}{31}{section.6}
    59 \contentsline {subsection}{\numberline {6.1}Labelled ${\sf Clight}$ and labelled ${\sf Cminor}$}{31}{subsection.6.1}
    60 \contentsline {subsection}{\numberline {6.2}Labels in ${\sf RTLAbs}$ and the back-end languages}{32}{subsection.6.2}
    61 \contentsline {subsection}{\numberline {6.3}Labelling of the source language}{32}{subsection.6.3}
    62 \contentsline {subsubsection}{\numberline {6.3.1}Sequential instructions}{32}{subsubsection.6.3.1}
    63 \contentsline {subsubsection}{\numberline {6.3.2}Ternary expressions}{32}{subsubsection.6.3.2}
    64 \contentsline {paragraph}{Related cases.}{33}{section*.17}
    65 \contentsline {subsubsection}{\numberline {6.3.3}Conditionals}{33}{subsubsection.6.3.3}
    66 \contentsline {subsubsection}{\numberline {6.3.4}Loops}{33}{subsubsection.6.3.4}
    67 \contentsline {subsubsection}{\numberline {6.3.5}Program Labels and Gotos}{34}{subsubsection.6.3.5}
    68 \contentsline {subsubsection}{\numberline {6.3.6}Function calls}{34}{subsubsection.6.3.6}
    69 \contentsline {subsection}{\numberline {6.4}Verifications on the object code}{35}{subsection.6.4}
    70 \contentsline {subsection}{\numberline {6.5}Building the cost annotation}{35}{subsection.6.5}
    71 \contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}
    72 \contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}
    73 \contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}
    74 \contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}
    75 \contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}
    76 \contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {soundness-small-step}}{40}{subsection.B.2}
    77 \contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {labelled-simulation-vm-mips}}{41}{subsection.B.3}
    78 \contentsline {paragraph}{The memory realisation.}{41}{section*.19}
    79 \contentsline {paragraph}{The inequation.}{41}{section*.20}
    80 \contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {annot-composition}}{41}{subsection.B.4}
    81 \contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {labelled-sim-imp-vm}}{42}{subsection.B.5}
    82 \contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {sim-vm-mips-prop}}{42}{subsection.B.6}
    83 \contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {lab-instr-erasure-imp}}{42}{subsection.B.7}
    84 \contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {global-commutation-prop}}{42}{subsection.B.8}
    85 \contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {instrument-to-label-prop}}{42}{subsection.B.9}
    86 \contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {sound-label-prop}}{43}{subsection.B.10}
    87 \contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {precise-label-prop}}{43}{subsection.B.11}
    88 \contentsline {subsection}{\numberline {B.12}Proof of proposition \ref {lab-sound}}{43}{subsection.B.12}
    89 \contentsline {subsection}{\numberline {B.13}Proof of proposition \ref {ann-correct}}{43}{subsection.B.13}
Note: See TracChangeset for help on using the changeset viewer.