..\..\tools\Dafny\Dafny.exe /noVerify /compile:2 /spillTargetCode:1 Libraries\Crypto\Hash\sha_test.i.dfy Libraries\Util\arrays_and_seqs.i.dfy Libraries\Util\be_sequences.s.dfy Libraries\Util\bytes_and_words.s.dfy Libraries\Util\integer_sequences.i.dfy Libraries\Util\integer_sequences.s.dfy Libraries\Util\integer_sequences_premium.i.dfy Libraries\Util\relational.s.dfy Libraries\Util\repeat_digit.i.dfy Libraries\Util\seqs_and_ints.i.dfy Libraries\Util\seqs_reverse.i.dfy Libraries\Util\seqs_simple.i.dfy Libraries\Util\seqs_transforms.i.dfy Libraries\Util\seq_blocking.i.dfy Libraries\Util\seq_blocking.s.dfy Libraries\Util\word_bits.i.dfy Libraries\Crypto\Hash\hmac_common.i.dfy Libraries\Crypto\Hash\hmac_common.s.dfy Libraries\Crypto\Hash\sha256.i.dfy Libraries\Crypto\Hash\sha256.s.dfy Libraries\Crypto\Hash\sha256_hmac.i.dfy Libraries\Crypto\Hash\sha_common.s.dfy Libraries\Crypto\Hash\sha_padding.i.dfy Libraries\Math\div.i.dfy Libraries\Math\div_boogie.i.dfy Libraries\Math\div_def.i.dfy Libraries\Math\evenodd.i.dfy Libraries\Math\mul.i.dfy Libraries\Math\power.i.dfy Libraries\Math\power.s.dfy Libraries\Math\power2.i.dfy Libraries\Math\power2.s.dfy Libraries\Math\round.i.dfy Drivers\CPU\assembly.s.dfy Drivers\CPU\assembly.i.dfy Drivers\CPU\assembly_premium.i.dfy Libraries\base.s.dfy Libraries\Crypto\Hash\sha1.s.dfy Libraries\Crypto\Hash\sha1.i.dfy Libraries\Crypto\Hash\sha1_hmac.i.dfy

