Ignore:
Timestamp:
Jun 15, 2012, 5:56:30 PM (7 years ago)
Author:
boender
Message:
  • added reference to Intel dev manual
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/proof.tex

    r2098 r2099  
    128128\end{lstlisting}
    129129
    130 This is a temporary formulation of the main property
     130This is a temporary formulation of the main property\\
    131131({\tt sigma\_policy\_specification}); its main difference
    132132from the final version is that it uses {\tt instruction\_size\_jmplen} to
     
    236236
    237237If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
    238 {\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase},
     238{\tt out\_of\_program\_none},\\
     239{\tt not\_jump\_default}, {\tt jump\_increase},
    239240and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
    240241retained without change.
Note: See TracChangeset for help on using the changeset viewer.