History log of /seL4-l4v-10.1.1/HOL4/examples/Crypto/TEA/teaScript.sml
Revision Date Author Comments
# 8d83067c 21-Oct-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove TABs from examples


# 97475109 27-Jul-2012 Michael Norrish <michael.norrish@nicta.com.au>

Remove trailing whitespace in examples directory.


# 21ac9716 11-Jun-2012 Konrad Slind <konrad.slind@gmail.com>

Correct right-shift operation in Crypt/TEA.

Now use Logical shift right (in HOL >>>). Before, arithmetic shift
right (in HOL >>) was used. It looked like the C I was working from,
but had different semantics. Once again a reason to hate and distrust
overloading (in C this time, but its good to hate overloading
universally).

Thanks to David Hardin for noticing this bug.


# c27de653 11-Jun-2009 Michael Norrish <Michael.Norrish@nicta.com.au>

Comment out generation/emission of ML code for SHA-1 and TEA. The
emitted files were bogus, and caused compilation to fail in
src/emit/ML. This latter directory isn't normally compiled at all,
but the ordinal example is set up to depend on it, so it ends up being
compiled when Holmake calls itself recursively.


# 84c7e529 11-Jun-2009 Michael Norrish <Michael.Norrish@nicta.com.au>

Get TEA to half-build, again failing to get ML emission correct.
Rather than attempt to have ML code emitted into this directory, where
it will then confuse Holmake, I follow the SHA1 example, and push it
off to src/emit/ML (except that it again complains about words$n2w).
This removes the need for the Holmakefile.


# 93b90a3e 16-May-2008 Konrad Slind <konrad.slind@gmail.com>

Slight mods.


# 5449fad7 12-May-2008 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Make use of WORDS_EMIT_RULE.


# 01d36a6e 12-May-2008 Konrad Slind <konrad.slind@gmail.com>

Mods to tea. Some more yet to come, as soon as I figure out
how to interface with wordsML.