everest-20161208105919.err

[NOTE] Package ppx_deriving is already installed (current version is 4.1).
[NOTE] Package ppx_deriving_yojson is already installed (current version is
       3.0).
[NOTE] Package zarith is already installed (current version is 1.4.1).
[NOTE] Package pprint is already installed (current version is 20140424).
[NOTE] Package process is already installed (current version is 0.2.1).
[NOTE] Package fileutils is already installed (current version is 0.5.1).
[NOTE] Package stdint is already installed (current version is 0.3.0-0).
[NOTE] Package batteries is already installed (current version is 2.5.3).
[NOTE] Package sqlite3 is already installed (current version is 4.0.5).
[NOTE] Package menhir is already installed (current version is 20161115).
[NOTE] Package fix is already installed (current version is 20130611).
[NOTE] Package sedlex is already installed (current version is 1.99.3).
[NOTE] Package ctypes is already installed (current version is 0.11.1).
[NOTE] Package ulex is already installed (current version is 1.1).
[NOTE] Package depext-cygwinports is already installed (current version is
       0.0.6).
Already on 'adl_lowlevel_merge'
Cloning into 'Spartan'...
Host key verification failed.
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.
Cloning into 'Spartan'...
fatal: could not read Username for 'https://msresearch.visualstudio.com': terminal prompts disabled
Already on 'c_record_aead'
Already on 'jk_low_level_crypto'
Already on 'master'
make[1]: warning: -jN forced in submake: disabling jobserver mode.
Warning: you are using the standard library and/or the %inline keyword. We
recommend switching on --infer in order to avoid obscure type error messages.
Warning 6: in the definition of buf, after the definition of m0, in top-level declaration Crypto.Symmetric.Bytes.random_bytes, in file Crypto_Symmetric_Bytes: stack newbuf 0uint8 @1 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES.cipher, in file Crypto_Symmetric_AES: stack newbuf 0uint8 Crypto.Symmetric.AES.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES.inv_cipher, in file Crypto_Symmetric_AES: stack newbuf 0uint8 Crypto.Symmetric.AES.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES128.cipher, in file Crypto_Symmetric_AES128: stack newbuf 0uint8 Crypto.Symmetric.AES128.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES128.inv_cipher, in file Crypto_Symmetric_AES128: stack newbuf 0uint8 Crypto.Symmetric.AES128.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in top-level declaration Crypto.Symmetric.MAC.rcreate, in file Crypto_Symmetric_MAC: eternal newbuf 0uint8 Crypto.Symmetric.MAC.wlen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of k, in top-level declaration Crypto.Symmetric.UF1CMA.akey_gen, in file Crypto_Symmetric_UF1CMA: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.skeylen @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of sk, in top-level declaration Crypto.Symmetric.UF1CMA.akey_coerce, in file Crypto_Symmetric_UF1CMA: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.skeylen @1 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of k, after the definition of len, in top-level declaration Crypto.Symmetric.UF1CMA.gen, in file Crypto_Symmetric_UF1CMA: eternal newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in top-level declaration Crypto.Plain.create, in file Crypto_Plain: stack newbuf @1 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keystate, after the definition of mac_rgn, in top-level declaration Crypto.Symmetric.PRF.gen, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.PRF.statelen @1 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of key, after the definition of keystate, in top-level declaration Crypto.Symmetric.PRF.gen, in file Crypto_Symmetric_PRF: stack newbuf 0uint8 Crypto.Symmetric.PRF.keylen @2 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keystate, after the definition of mac_rgn, in top-level declaration Crypto.Symmetric.PRF.coerce, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.PRF.statelen @2 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keyBuffer, after the definition of macId, in top-level declaration Crypto.Symmetric.PRF.prf_mac, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.keylen @6 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keyBuffer, after the definition of x, in top-level declaration Crypto.Symmetric.PRF.prf_sk0, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.skeylen @3 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of cipher, after the definition of cipherlen, in top-level declaration Crypto.KrmlTest.test, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of cipher, after the definition of cipherlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm, in file Crypto_KrmlTest: stack newbuf 2uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of plain, after the definition of plainlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_0, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_0, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of plain, after the definition of plainlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_1, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_1, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of plain, after the definition of plainlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_2, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_2, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_3, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 3: run_or_warn: the following command failed:
x86_64-w64-mingw32-gcc -Wno-unused-but-set-variable -std=c11 -Wall -Werror -Wno-parentheses -Wno-unused-variable -g -O3 -fwrapv -I FSTAR_HOME/ulib/hyperstack -I spartan_aes -I crypto -I ../../../kremlin/kremlib -I ../../../kremlin/test -I C:/Build/Agent/_work/30/s/kremlin/kremlib -I tmp -maes -Wno-error=pointer-sign -c crypto/spartan_stub.c -o tmp/spartan_stub.o
Warning 3: run_or_warn: the following command failed:
x86_64-w64-mingw32-gcc -Wno-unused-but-set-variable -std=c11 -Wall -Werror -Wno-parentheses -Wno-unused-variable -g -O3 -fwrapv -I FSTAR_HOME/ulib/hyperstack -I spartan_aes -I crypto -I ../../../kremlin/kremlib -I ../../../kremlin/test -I C:/Build/Agent/_work/30/s/kremlin/kremlib -I tmp -maes -Wno-error=pointer-sign tmp/Prims.o tmp/FStar_Mul.o tmp/FStar_Squash.o tmp/FStar_StrongExcludedMiddle.o tmp/FStar_List_Tot.o tmp/FStar_Classical.o tmp/FStar_ListProperties.o tmp/FStar_SeqProperties.o tmp/FStar_Math_Lemmas.o tmp/FStar_BitVector.o tmp/FStar_UInt.o tmp/FStar_Int.o tmp/FStar_FunctionalExtensionality.o tmp/FStar_PropositionalExtensionality.o tmp/FStar_PredicateExtensionality.o tmp/FStar_TSet.o tmp/FStar_Set.o tmp/FStar_Map.o tmp/FStar_Ghost.o tmp/FStar_All.o tmp/FStar_Bytes.o tmp/FStar_Buffer.o tmp/Buffer_Utils.o tmp/Crypto_Symmetric_Bytes.o tmp/Crypto_Symmetric_Poly1305_Spec.o tmp/Crypto_Symmetric_Poly1305_Parameters.o tmp/Crypto_Symmetric_Poly1305_Bigint.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part1.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part2.o tmp/Crypto_AEAD_BufferUtils.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part3.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part4.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part5.o tmp/FStar_Buffer_Quantifiers.o tmp/Crypto_Symmetric_Chacha20.o tmp/Crypto_Config.o tmp/Crypto_Indexing.o tmp/Flag.o tmp/Crypto_Symmetric_AES.o tmp/Spartan.o tmp/Crypto_Symmetric_AES128.o tmp/Crypto_Symmetric_Cipher.o tmp/Crypto_Symmetric_Poly1305_Lemmas.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part6.o tmp/Crypto_Symmetric_Poly1305_Bignum.o tmp/Crypto_Symmetric_Poly1305.o tmp/Crypto_Symmetric_GF128_Spec.o tmp/Crypto_Symmetric_GF128.o tmp/Crypto_Symmetric_MAC.o tmp/Crypto_Symmetric_UF1CMA.o tmp/Crypto_Plain.o tmp/Crypto_Symmetric_PRF.o tmp/Crypto_AEAD_Encoding.o tmp/Crypto_AEAD_Invariant.o tmp/Crypto_AEAD_Lemmas.o tmp/Crypto_AEAD_Lemmas_Part2.o tmp/Crypto_AEAD_Lemmas_Part3.o tmp/Crypto_AEAD_Wrappers.o tmp/Crypto_AEAD.o tmp/Crypto_KrmlTest.o tmp/kremlib.o tmp/test_hacks.o tmp/testlib.o spartan_aes/aes.o -o krml-test.exe
make: *** [Makefile:202: krml-test.exe] Error 250
make[2]: warning: jobserver unavailable: using -j1.  Add '+' to parent make rule.
make[2]: warning: jobserver unavailable: using -j1.  Add '+' to parent make rule.
make[2]: warning: jobserver unavailable: using -j1.  Add '+' to parent make rule.
Warning 6: in the definition of buf, after the definition of m0, in top-level declaration Crypto.Symmetric.Bytes.random_bytes, in file Crypto_Symmetric_Bytes: stack newbuf 0uint8 @1 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES.cipher, in file Crypto_Symmetric_AES: stack newbuf 0uint8 Crypto.Symmetric.AES.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES.inv_cipher, in file Crypto_Symmetric_AES: stack newbuf 0uint8 Crypto.Symmetric.AES.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES128.cipher, in file Crypto_Symmetric_AES128: stack newbuf 0uint8 Crypto.Symmetric.AES128.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of state, in top-level declaration Crypto.Symmetric.AES128.inv_cipher, in file Crypto_Symmetric_AES128: stack newbuf 0uint8 Crypto.Symmetric.AES128.blocklen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in top-level declaration Crypto.Symmetric.MAC.rcreate, in file Crypto_Symmetric_MAC: eternal newbuf 0uint8 Crypto.Symmetric.MAC.wlen is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of k, in top-level declaration Crypto.Symmetric.UF1CMA.akey_gen, in file Crypto_Symmetric_UF1CMA: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.skeylen @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of sk, in top-level declaration Crypto.Symmetric.UF1CMA.akey_coerce, in file Crypto_Symmetric_UF1CMA: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.skeylen @1 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of k, after the definition of len, in top-level declaration Crypto.Symmetric.UF1CMA.gen, in file Crypto_Symmetric_UF1CMA: eternal newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in top-level declaration Crypto.Plain.create, in file Crypto_Plain: stack newbuf @1 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keystate, after the definition of mac_rgn, in top-level declaration Crypto.Symmetric.PRF.gen, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.PRF.statelen @1 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of key, after the definition of keystate, in top-level declaration Crypto.Symmetric.PRF.gen, in file Crypto_Symmetric_PRF: stack newbuf 0uint8 Crypto.Symmetric.PRF.keylen @2 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keystate, after the definition of mac_rgn, in top-level declaration Crypto.Symmetric.PRF.coerce, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.PRF.statelen @2 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keyBuffer, after the definition of macId, in top-level declaration Crypto.Symmetric.PRF.prf_mac, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.keylen @6 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of keyBuffer, after the definition of x, in top-level declaration Crypto.Symmetric.PRF.prf_sk0, in file Crypto_Symmetric_PRF: eternal newbuf 0uint8 Crypto.Symmetric.UF1CMA.skeylen @3 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of cipher, after the definition of cipherlen, in top-level declaration Crypto.KrmlTest.test, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of cipher, after the definition of cipherlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm, in file Crypto_KrmlTest: stack newbuf 2uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of plain, after the definition of plainlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_0, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_0, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of plain, after the definition of plainlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_1, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_1, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of plain, after the definition of plainlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_2, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_2, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 6: in the definition of aad, after the definition of aadlen, in top-level declaration Crypto.KrmlTest.test_aes_gcm_3, in file Crypto_KrmlTest: stack newbuf 0uint8 @0 is a non-constant size, stack-allocated array; this is not supported by CompCert
Warning 3: run_or_warn: the following command failed:
x86_64-w64-mingw32-gcc -Wno-unused-but-set-variable -std=c11 -Wall -Werror -Wno-parentheses -Wno-unused-variable -g -O3 -fwrapv -I FSTAR_HOME/ulib/hyperstack -I spartan_aes -I crypto -I ../../../kremlin/kremlib -I ../../../kremlin/test -I C:/Build/Agent/_work/30/s/kremlin/kremlib -I tmp -maes -Wno-error=pointer-sign -c crypto/spartan_stub.c -o tmp/spartan_stub.o
Warning 3: run_or_warn: the following command failed:
x86_64-w64-mingw32-gcc -Wno-unused-but-set-variable -std=c11 -Wall -Werror -Wno-parentheses -Wno-unused-variable -g -O3 -fwrapv -I FSTAR_HOME/ulib/hyperstack -I spartan_aes -I crypto -I ../../../kremlin/kremlib -I ../../../kremlin/test -I C:/Build/Agent/_work/30/s/kremlin/kremlib -I tmp -maes -Wno-error=pointer-sign tmp/Prims.o tmp/FStar_Mul.o tmp/FStar_Squash.o tmp/FStar_StrongExcludedMiddle.o tmp/FStar_List_Tot.o tmp/FStar_Classical.o tmp/FStar_ListProperties.o tmp/FStar_SeqProperties.o tmp/FStar_Math_Lemmas.o tmp/FStar_BitVector.o tmp/FStar_UInt.o tmp/FStar_Int.o tmp/FStar_FunctionalExtensionality.o tmp/FStar_PropositionalExtensionality.o tmp/FStar_PredicateExtensionality.o tmp/FStar_TSet.o tmp/FStar_Set.o tmp/FStar_Map.o tmp/FStar_Ghost.o tmp/FStar_All.o tmp/FStar_Bytes.o tmp/FStar_Buffer.o tmp/Buffer_Utils.o tmp/Crypto_Symmetric_Bytes.o tmp/Crypto_Symmetric_Poly1305_Spec.o tmp/Crypto_Symmetric_Poly1305_Parameters.o tmp/Crypto_Symmetric_Poly1305_Bigint.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part1.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part2.o tmp/Crypto_AEAD_BufferUtils.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part3.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part4.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part5.o tmp/FStar_Buffer_Quantifiers.o tmp/Crypto_Symmetric_Chacha20.o tmp/Crypto_Config.o tmp/Crypto_Indexing.o tmp/Flag.o tmp/Crypto_Symmetric_AES.o tmp/Spartan.o tmp/Crypto_Symmetric_AES128.o tmp/Crypto_Symmetric_Cipher.o tmp/Crypto_Symmetric_Poly1305_Lemmas.o tmp/Crypto_Symmetric_Poly1305_Bignum_Lemmas_Part6.o tmp/Crypto_Symmetric_Poly1305_Bignum.o tmp/Crypto_Symmetric_Poly1305.o tmp/Crypto_Symmetric_GF128_Spec.o tmp/Crypto_Symmetric_GF128.o tmp/Crypto_Symmetric_MAC.o tmp/Crypto_Symmetric_UF1CMA.o tmp/Crypto_Plain.o tmp/Crypto_Symmetric_PRF.o tmp/Crypto_AEAD_Encoding.o tmp/Crypto_AEAD_Invariant.o tmp/Crypto_AEAD_Lemmas.o tmp/Crypto_AEAD_Lemmas_Part2.o tmp/Crypto_AEAD_Lemmas_Part3.o tmp/Crypto_AEAD_Wrappers.o tmp/Crypto_AEAD.o tmp/Crypto_KrmlTest.o tmp/kremlib.o tmp/test_hacks.o tmp/testlib.o spartan_aes/aes.o -o krml-test.exe
make[2]: *** [Makefile:202: krml-test.exe] Error 250
make[1]: *** [Makefile:67: ../krml-test.exe] Error 2
make: *** [Makefile:345: tls-gen-spartan] Error 2