xref: /aoo41x/main/nss/nss_win.patch (revision 0ae430aa)

--- misc/nss-3.39/nss/cmd/signtool/sign.c	2016-06-20 14:11:28.000000000 -0300
+++ misc/build/nss-3.39/nss/cmd/signtool/sign.c	2019-11-01 13:32:56.496828470 -0300
@@ -8,6 +8,10 @@
 #include "blapi.h"
 #include "sechash.h" /* for HASH_GetHashObject() */

+#if defined(_MSC_VER) && _MSC_VER < 1900
+#define snprintf _snprintf
+#endif
+
 static int create_pk7(char *dir, char *keyName, int *keyType);
 static int jar_find_key_type(CERTCertificate *cert);
 static int manifesto(char *dirname, char *install_script, PRBool recurse);
diff -ur misc/nss-3.39/nss/cmd/Makefile misc/build/nss-3.39/nss/cmd/Makefile
--- misc/nss-3.39/nss/cmd/Makefile	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/cmd/Makefile	2018-10-22 14:53:30.297923000 -0700
@@ -21,7 +21,8 @@
 FIPSTEST_SRCDIR =
 SHLIBSIGN_SRCDIR =
 else
-BLTEST_SRCDIR = bltest
+# BLTEST_SRCDIR = bltest
+BLTEST_SRCDIR =
 ECPERF_SRCDIR = ecperf
 FREEBL_ECTEST_SRCDIR = fbectest
 FIPSTEST_SRCDIR = fipstest
diff -ur misc/nss-3.39/nss/cmd/lib/secutil.c misc/build/nss-3.39/nss/cmd/lib/secutil.c
--- misc/nss-3.39/nss/cmd/lib/secutil.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/cmd/lib/secutil.c	2018-10-22 10:44:05.694582000 -0700
@@ -217,6 +217,7 @@
     secuPWData *pwdata = (secuPWData *)arg;
     secuPWData pwnull = { PW_NONE, 0 };
     secuPWData pwxtrn = { PW_EXTERNAL, "external" };
+    char *pw;

     if (pwdata == NULL)
         pwdata = &pwnull;
@@ -240,7 +241,7 @@
             sprintf(prompt,
                     "Press Enter, then enter PIN for \"%s\" on external device.\n",
                     PK11_GetTokenName(slot));
-            char *pw = SECU_GetPasswordString(NULL, prompt);
+            pw = SECU_GetPasswordString(NULL, prompt);
             PORT_Free(pw);
         /* Fall Through */
         case PW_PLAINTEXT:
@@ -3841,10 +3842,11 @@
 countItems(const char *arg, unsigned int *numItems)
 {
     char *str = PORT_Strdup(arg);
+    char *p;
     if (!str) {
         return SECFailure;
     }
-    char *p = strtok(str, ",");
+    p = strtok(str, ",");
     while (p) {
         ++(*numItems);
         p = strtok(NULL, ",");
@@ -3943,6 +3945,8 @@
     SSLSignatureScheme *schemes;
     unsigned int numValues = 0;
     unsigned int count = 0;
+    char *str;
+    char *p;

     if (countItems(arg, &numValues) != SECSuccess) {
         return SECFailure;
@@ -3953,11 +3957,11 @@
     }

     /* Get group names. */
-    char *str = PORT_Strdup(arg);
+    str = PORT_Strdup(arg);
     if (!str) {
         goto done;
     }
-    char *p = strtok(str, ",");
+    p = strtok(str, ",");
     while (p) {
         SSLSignatureScheme scheme = schemeNameToScheme(p);
         if (scheme == ssl_sig_none) {
diff -ur misc/nss-3.39/nss/cmd/signtool/javascript.c misc/build/nss-3.39/nss/cmd/signtool/javascript.c
--- misc/nss-3.39/nss/cmd/signtool/javascript.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/cmd/signtool/javascript.c	2018-10-22 15:02:16.878938000 -0700
@@ -1672,7 +1672,7 @@
 {
     char fn[FNSIZE];
     PRDir *dir;
-    int c = snprintf(fn, sizeof(fn), "%s/%s", basepath, path);
+    int c = PR_snprintf(fn, sizeof(fn), "%s/%s", basepath, path);
     if (c >= sizeof(fn)) {
         return PR_FAILURE;
     }
diff -ur misc/nss-3.39/nss/cmd/signtool/sign.c misc/build/nss-3.39/nss/cmd/signtool/sign.c
--- misc/nss-3.39/nss/cmd/signtool/sign.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/cmd/signtool/sign.c	2018-10-22 15:01:53.353243000 -0700
@@ -82,13 +82,13 @@
         }

         /* rsa/dsa to zip */
-        count = snprintf(tempfn, sizeof(tempfn), "META-INF/%s.%s", base, (keyType == dsaKey ? "dsa" : "rsa"));
+        count = PR_snprintf(tempfn, sizeof(tempfn), "META-INF/%s.%s", base, (keyType == dsaKey ? "dsa" : "rsa"));
         if (count >= sizeof(tempfn)) {
             PR_fprintf(errorFD, "unable to write key metadata\n");
             errorCount++;
             exit(ERRX);
         }
-        count = snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
+        count = PR_snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
         if (count >= sizeof(fullfn)) {
             PR_fprintf(errorFD, "unable to write key metadata\n");
             errorCount++;
@@ -103,7 +103,7 @@
     }
     /* mf to zip */
     strcpy(tempfn, "META-INF/manifest.mf");
-    count = snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
+    count = PR_snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
     if (count >= sizeof(fullfn)) {
         PR_fprintf(errorFD, "unable to write manifest\n");
         errorCount++;
@@ -112,13 +112,13 @@
     JzipAdd(fullfn, tempfn, zipfile, compression_level);

     /* sf to zip */
-    count = snprintf(tempfn, sizeof(tempfn), "META-INF/%s.sf", base);
+    count = PR_snprintf(tempfn, sizeof(tempfn), "META-INF/%s.sf", base);
     if (count >= sizeof(tempfn)) {
         PR_fprintf(errorFD, "unable to write sf metadata\n");
         errorCount++;
         exit(ERRX);
     }
-    count = snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
+    count = PR_snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
     if (count >= sizeof(fullfn)) {
         PR_fprintf(errorFD, "unable to write sf metadata\n");
         errorCount++;
@@ -129,13 +129,13 @@
     /* Add the rsa/dsa file to the zip archive normally */
     if (!xpi_arc) {
         /* rsa/dsa to zip */
-        count = snprintf(tempfn, sizeof(tempfn), "META-INF/%s.%s", base, (keyType == dsaKey ? "dsa" : "rsa"));
+        count = PR_snprintf(tempfn, sizeof(tempfn), "META-INF/%s.%s", base, (keyType == dsaKey ? "dsa" : "rsa"));
         if (count >= sizeof(tempfn)) {
             PR_fprintf(errorFD, "unable to write key metadata\n");
             errorCount++;
             exit(ERRX);
         }
-        count = snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
+        count = PR_snprintf(fullfn, sizeof(fullfn), "%s/%s", tree, tempfn);
         if (count >= sizeof(fullfn)) {
             PR_fprintf(errorFD, "unable to write key metadata\n");
             errorCount++;
@@ -456,7 +456,7 @@
         if (!PL_HashTableLookup(extensions, ext))
             return 0;
     }
-    count = snprintf(fullname, sizeof(fullname), "%s/%s", basedir, relpath);
+    count = PR_snprintf(fullname, sizeof(fullname), "%s/%s", basedir, relpath);
     if (count >= sizeof(fullname)) {
         return 1;
     }
diff -ur misc/nss-3.39/nss/gtests/freebl_gtest/kat/blake2b_kat.h misc/build/nss-3.39/nss/gtests/freebl_gtest/kat/blake2b_kat.h
--- misc/nss-3.39/nss/gtests/freebl_gtest/kat/blake2b_kat.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/gtests/freebl_gtest/kat/blake2b_kat.h	2018-10-21 01:47:24.131348000 -0700
@@ -5,7 +5,23 @@
 /* https://github.com/BLAKE2/BLAKE2/blob/master/testvectors/blake2b-kat.txt */

 #include <vector>
-#include <stdint.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #ifdef _WIN64
+typedef unsigned __int64 uintptr_t;
+ #else
+typedef unsigned int uintptr_t;
+ #endif
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned __int64 uint64_t;
+#define UINT8_MAX	0xff
+#define UINT16_MAX	0xffff
+#define UINT32_MAX	0xffffffffu
+#define UINT64_MAX	0xffffffffffffffffU
+#else
+ #include <stdint.h>
+#endif

 const std::vector<uint8_t> kat_key = {
     0,  1,  2,  3,  4,  5,  6,  7,  8,  9,  10, 11, 12, 13, 14, 15,
@@ -4643,4 +4659,4 @@
              0x10, 0x70, 0xfa, 0xa0, 0x37, 0x2a, 0xa4, 0x3e, 0x92, 0x48, 0x4b,
              0xe1, 0xc1, 0xe7, 0x3b, 0xa1, 0x09, 0x06, 0xd5, 0xd1, 0x85, 0x3d,
              0xb6, 0xa4, 0x10, 0x6e, 0x0a, 0x7b, 0xf9, 0x80, 0x0d, 0x37, 0x3d,
-             0x6d, 0xee, 0x2d, 0x46, 0xd6, 0x2e, 0xf2, 0xa4, 0x61}))};
\ No newline at end of file
+             0x6d, 0xee, 0x2d, 0x46, 0xd6, 0x2e, 0xf2, 0xa4, 0x61}))};
diff -ur misc/nss-3.39/nss/gtests/ssl_gtest/libssl_internals.h misc/build/nss-3.39/nss/gtests/ssl_gtest/libssl_internals.h
--- misc/nss-3.39/nss/gtests/ssl_gtest/libssl_internals.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/gtests/ssl_gtest/libssl_internals.h	2018-10-21 01:47:16.342484000 -0700
@@ -7,7 +7,23 @@
 #ifndef libssl_internals_h_
 #define libssl_internals_h_

-#include <stdint.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #ifdef _WIN64
+typedef unsigned __int64 uintptr_t;
+ #else
+typedef unsigned int uintptr_t;
+ #endif
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned __int64 uint64_t;
+#define UINT8_MAX	0xff
+#define UINT16_MAX	0xffff
+#define UINT32_MAX	0xffffffffu
+#define UINT64_MAX	0xffffffffffffffffU
+#else
+ #include <stdint.h>
+#endif

 #include "prio.h"
 #include "seccomon.h"
diff -ur misc/nss-3.39/nss/lib/freebl/blake2b.c misc/build/nss-3.39/nss/lib/freebl/blake2b.c
--- misc/nss-3.39/nss/lib/freebl/blake2b.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/blake2b.c	2018-10-21 15:08:03.065644000 -0700
@@ -147,6 +147,7 @@
 blake2b_Begin(BLAKE2BContext* ctx, uint8_t outlen, const uint8_t* key,
               size_t keylen)
 {
+    uint64_t param;
     PORT_Assert(ctx != NULL);
     if (!ctx) {
         goto failure;
@@ -164,7 +165,7 @@
     }

     /* Mix key size(keylen) and desired hash length(outlen) into h0 */
-    uint64_t param = outlen ^ (keylen << 8) ^ (1 << 16) ^ (1 << 24);
+    param = outlen ^ (keylen << 8) ^ (1 << 16) ^ (1 << 24);
     PORT_Memcpy(ctx->h, iv, 8 * 8);
     ctx->h[0] ^= param;
     ctx->outlen = outlen;
@@ -402,12 +403,13 @@
 BLAKE2BContext*
 BLAKE2B_Resurrect(unsigned char* space, void* arg)
 {
+    BLAKE2BContext* ctx;
     PORT_Assert(space != NULL);
     if (!space) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
         return NULL;
     }
-    BLAKE2BContext* ctx = BLAKE2B_NewContext();
+    ctx = BLAKE2B_NewContext();
     if (ctx == NULL) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
         return NULL;
diff -ur misc/nss-3.39/nss/lib/freebl/blake2b.h misc/build/nss-3.39/nss/lib/freebl/blake2b.h
--- misc/nss-3.39/nss/lib/freebl/blake2b.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/blake2b.h	2018-10-21 01:46:57.467020000 -0700
@@ -9,7 +9,23 @@
 #define BLAKE_H

 #include <stddef.h>
-#include <stdint.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #ifdef _WIN64
+typedef unsigned __int64 uintptr_t;
+ #else
+typedef unsigned int uintptr_t;
+ #endif
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned __int64 uint64_t;
+#define UINT8_MAX	0xff
+#define UINT16_MAX	0xffff
+#define UINT32_MAX	0xffffffffu
+#define UINT64_MAX	0xffffffffffffffffU
+#else
+ #include <stdint.h>
+#endif

 struct Blake2bContextStr {
     uint64_t h[8];                     /* chained state */
diff -ur misc/nss-3.39/nss/lib/freebl/chacha20poly1305.c misc/build/nss-3.39/nss/lib/freebl/chacha20poly1305.c
--- misc/nss-3.39/nss/lib/freebl/chacha20poly1305.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/chacha20poly1305.c	2018-10-21 21:01:18.295557000 -0700
@@ -77,14 +77,14 @@
         Hacl_Poly1305_mk_state(stateStack, stateStack + offset);

     unsigned char block[16] = { 0 };
+    unsigned int i;
+    unsigned int j;
     Hacl_Poly1305_init(state, (uint8_t *)key);

     Poly1305PadUpdate(state, block, ad, adLen);
     memset(block, 0, 16);
     Poly1305PadUpdate(state, block, ciphertext, ciphertextLen);

-    unsigned int i;
-    unsigned int j;
     for (i = 0, j = adLen; i < 8; i++, j >>= 8) {
         block[i] = j;
     }
diff -ur misc/nss-3.39/nss/lib/freebl/ecl/ecp_25519.c misc/build/nss-3.39/nss/lib/freebl/ecl/ecp_25519.c
--- misc/nss-3.39/nss/lib/freebl/ecl/ecp_25519.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/ecl/ecp_25519.c	2018-10-21 21:06:07.350639000 -0700
@@ -104,6 +104,7 @@
 {
     PRUint8 *px;
     PRUint8 basePoint[32] = { 9 };
+    SECStatus rv;

     if (!P) {
         px = basePoint;
@@ -115,7 +116,7 @@
         px = P->data;
     }

-    SECStatus rv = ec_Curve25519_mul(X->data, k->data, px);
+    rv = ec_Curve25519_mul(X->data, k->data, px);
     if (NSS_SecureMemcmpZero(X->data, X->len) == 0) {
         return SECFailure;
     }
diff -ur misc/nss-3.39/nss/lib/freebl/gcm.h misc/build/nss-3.39/nss/lib/freebl/gcm.h
--- misc/nss-3.39/nss/lib/freebl/gcm.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/gcm.h	2018-10-21 01:46:50.706497000 -0700
@@ -6,7 +6,23 @@
 #define GCM_H 1

 #include "blapii.h"
-#include <stdint.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #ifdef _WIN64
+typedef unsigned __int64 uintptr_t;
+ #else
+typedef unsigned int uintptr_t;
+ #endif
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned __int64 uint64_t;
+#define UINT8_MAX	0xff
+#define UINT16_MAX	0xffff
+#define UINT32_MAX	0xffffffffu
+#define UINT64_MAX	0xffffffffffffffffU
+#else
+ #include <stdint.h>
+#endif

 #ifdef NSS_X86_OR_X64
 /* GCC <= 4.8 doesn't support including emmintrin.h without enabling SSE2 */
diff -ur misc/nss-3.39/nss/lib/freebl/rijndael.h misc/build/nss-3.39/nss/lib/freebl/rijndael.h
--- misc/nss-3.39/nss/lib/freebl/rijndael.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/rijndael.h	2018-10-21 01:47:05.758087000 -0700
@@ -6,7 +6,23 @@
 #define _RIJNDAEL_H_ 1

 #include "blapii.h"
-#include <stdint.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #ifdef _WIN64
+typedef unsigned __int64 uintptr_t;
+ #else
+typedef unsigned int uintptr_t;
+ #endif
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned __int64 uint64_t;
+#define UINT8_MAX	0xff
+#define UINT16_MAX	0xffff
+#define UINT32_MAX	0xffffffffu
+#define UINT64_MAX	0xffffffffffffffffU
+#else
+ #include <stdint.h>
+#endif

 #if defined(NSS_X86_OR_X64)
 /* GCC <= 4.8 doesn't support including emmintrin.h without enabling SSE2 */
diff -ur misc/nss-3.39/nss/lib/freebl/verified/FStar.c misc/build/nss-3.39/nss/lib/freebl/verified/FStar.c
--- misc/nss-3.39/nss/lib/freebl/verified/FStar.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/FStar.c	2018-10-21 23:50:44.099188000 -0700
@@ -32,37 +32,37 @@
 FStar_UInt128_uint128
 FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return (
-        (FStar_UInt128_uint128){
-            .low = a.low + b.low,
-            .high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.low + b.low;
+    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
+    return (ret);
 }

 FStar_UInt128_uint128
 FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return (
-        (FStar_UInt128_uint128){
-            .low = a.low + b.low,
-            .high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.low + b.low;
+    ret.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
+    return (ret);
 }

 FStar_UInt128_uint128
 FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return (
-        (FStar_UInt128_uint128){
-            .low = a.low - b.low,
-            .high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.low - b.low;
+    ret.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
+    return (ret);
 }

 static FStar_UInt128_uint128
 FStar_UInt128_sub_mod_impl(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return (
-        (FStar_UInt128_uint128){
-            .low = a.low - b.low,
-            .high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.low - b.low;
+    ret.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
+    return (ret);
 }

 FStar_UInt128_uint128
@@ -74,25 +74,37 @@
 FStar_UInt128_uint128
 FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return ((FStar_UInt128_uint128){.low = a.low & b.low, .high = a.high & b.high });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.low & b.low;
+    ret.high = a.high & b.high;
+    return (ret);
 }

 FStar_UInt128_uint128
 FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return ((FStar_UInt128_uint128){.low = a.low ^ b.low, .high = a.high ^ b.high });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.low ^ b.low;
+    ret.high = a.high ^ b.high;
+    return (ret);
 }

 FStar_UInt128_uint128
 FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return ((FStar_UInt128_uint128){.low = a.low | b.low, .high = a.high | b.high });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.low | b.low;
+    ret.high = a.high | b.high;
+    return (ret);
 }

 FStar_UInt128_uint128
 FStar_UInt128_lognot(FStar_UInt128_uint128 a)
 {
-    return ((FStar_UInt128_uint128){.low = ~a.low, .high = ~a.high });
+    FStar_UInt128_uint128 ret;
+    ret.low = ~a.low;
+    ret.high = ~a.high;
+    return (ret);
 }

 static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
@@ -112,19 +124,23 @@
 static FStar_UInt128_uint128
 FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)
 {
+    FStar_UInt128_uint128 ret;
     if (s == (uint32_t)0U)
         return a;
-    else
-        return (
-            (FStar_UInt128_uint128){
-                .low = a.low << s,
-                .high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s) });
+    else {
+        ret.low = a.low << s;
+        ret.high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s);
+        return (ret);
+   }
 }

 static FStar_UInt128_uint128
 FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)
 {
-    return ((FStar_UInt128_uint128){.low = (uint64_t)0U, .high = a.low << (s - FStar_UInt128_u32_64) });
+    FStar_UInt128_uint128 ret;
+    ret.low = (uint64_t)0U;
+    ret.high = a.low << (s - FStar_UInt128_u32_64);
+    return (ret);
 }

 FStar_UInt128_uint128
@@ -151,19 +167,23 @@
 static FStar_UInt128_uint128
 FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)
 {
+    FStar_UInt128_uint128 ret;
     if (s == (uint32_t)0U)
         return a;
-    else
-        return (
-            (FStar_UInt128_uint128){
-                .low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s),
-                .high = a.high >> s });
+    else {
+        ret.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s);
+        ret.high = a.high >> s;
+        return (ret);
+    }
 }

 static FStar_UInt128_uint128
 FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)
 {
-    return ((FStar_UInt128_uint128){.low = a.high >> (s - FStar_UInt128_u32_64), .high = (uint64_t)0U });
+    FStar_UInt128_uint128 ret;
+    ret.low = a.high >> (s - FStar_UInt128_u32_64);
+    ret.high = (uint64_t)0U;
+    return (ret);
 }

 FStar_UInt128_uint128
@@ -178,25 +198,28 @@
 FStar_UInt128_uint128
 FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return (
-        (FStar_UInt128_uint128){
-            .low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high),
-            .high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high) });
+    FStar_UInt128_uint128 ret;
+    ret.low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high);
+    ret.high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high);
+    return (ret);
 }

 FStar_UInt128_uint128
 FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
 {
-    return (
-        (FStar_UInt128_uint128){
-            .low = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)),
-            .high = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low)) });
+    FStar_UInt128_uint128 ret;
+    ret.low = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low));
+    ret.high = (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high)) | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low));
+    return (ret);
 }

 FStar_UInt128_uint128
 FStar_UInt128_uint64_to_uint128(uint64_t a)
 {
-    return ((FStar_UInt128_uint128){.low = a, .high = (uint64_t)0U });
+    FStar_UInt128_uint128 ret;
+    ret.low = a;
+    ret.high = (uint64_t)0U;
+    return (ret);
 }

 uint64_t
@@ -218,12 +241,13 @@
 static K___uint64_t_uint64_t_uint64_t_uint64_t
 FStar_UInt128_mul_wide_impl_t_(uint64_t x, uint64_t y)
 {
-    return (
-        (K___uint64_t_uint64_t_uint64_t_uint64_t){
-            .fst = FStar_UInt128_u64_mod_32(x),
-            .snd = FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y)),
-            .thd = x >> FStar_UInt128_u32_32,
-            .f3 = (x >> FStar_UInt128_u32_32) * FStar_UInt128_u64_mod_32(y) + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32) });
+
+    K___uint64_t_uint64_t_uint64_t_uint64_t ret;
+    ret.fst = FStar_UInt128_u64_mod_32(x);
+    ret.snd = FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y));
+    ret.thd = x >> FStar_UInt128_u32_32;
+    ret.f3 = (x >> FStar_UInt128_u32_32) * FStar_UInt128_u64_mod_32(y) + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32);
+    return (ret);
 }

 static uint64_t
@@ -240,12 +264,12 @@
     uint64_t w3 = scrut.snd;
     uint64_t x_ = scrut.thd;
     uint64_t t_ = scrut.f3;
-    return (
-        (FStar_UInt128_uint128){
-            .low = FStar_UInt128_u32_combine_(u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_),
-                                              w3),
-            .high = x_ * (y >> FStar_UInt128_u32_32) + (t_ >> FStar_UInt128_u32_32) +
-                    ((u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_)) >> FStar_UInt128_u32_32) });
+    FStar_UInt128_uint128 ret;
+    ret.low = FStar_UInt128_u32_combine_(u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_),
+                                              w3);
+    ret.high = x_ * (y >> FStar_UInt128_u32_32) + (t_ >> FStar_UInt128_u32_32) +
+                    ((u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_)) >> FStar_UInt128_u32_32);
+    return (ret);
 }

 FStar_UInt128_uint128
diff -ur misc/nss-3.39/nss/lib/freebl/verified/FStar.h misc/build/nss-3.39/nss/lib/freebl/verified/FStar.h
--- misc/nss-3.39/nss/lib/freebl/verified/FStar.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/FStar.h	2018-10-21 23:03:05.151005000 -0700
@@ -17,6 +17,7 @@
 #ifndef __FStar_H
 #define __FStar_H

+#include "secport.h"
 #include "kremlib_base.h"

 typedef struct
diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.c misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.c
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.c	2018-10-21 21:47:24.553180000 -0700
@@ -18,7 +18,8 @@
 static void
 Hacl_Lib_LoadStore32_uint32s_from_le_bytes(uint32_t *output, uint8_t *input, uint32_t len)
 {
-    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
         uint8_t *x0 = input + (uint32_t)4U * i;
         uint32_t inputi = load32_le(x0);
         output[i] = inputi;
@@ -28,7 +29,8 @@
 static void
 Hacl_Lib_LoadStore32_uint32s_to_le_bytes(uint8_t *output, uint32_t *input, uint32_t len)
 {
-    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
         uint32_t hd1 = input[i];
         uint8_t *x0 = output + (uint32_t)4U * i;
         store32_le(x0, hd1);
@@ -46,31 +48,49 @@
 {
     uint32_t sa = st[a];
     uint32_t sb0 = st[b];
+    uint32_t sd;
+    uint32_t sa10;
+    uint32_t sda;
+    uint32_t sa0;
+    uint32_t sb1;
+    uint32_t sd0;
+    uint32_t sa11;
+    uint32_t sda0;
+    uint32_t sa2;
+    uint32_t sb2;
+    uint32_t sd1;
+    uint32_t sa12;
+    uint32_t sda1;
+    uint32_t sa3;
+    uint32_t sb;
+    uint32_t sd2;
+    uint32_t sa1;
+    uint32_t sda2;
     st[a] = sa + sb0;
-    uint32_t sd = st[d];
-    uint32_t sa10 = st[a];
-    uint32_t sda = sd ^ sa10;
+    sd = st[d];
+    sa10 = st[a];
+    sda = sd ^ sa10;
     st[d] = Hacl_Impl_Chacha20_rotate_left(sda, (uint32_t)16U);
-    uint32_t sa0 = st[c];
-    uint32_t sb1 = st[d];
+    sa0 = st[c];
+    sb1 = st[d];
     st[c] = sa0 + sb1;
-    uint32_t sd0 = st[b];
-    uint32_t sa11 = st[c];
-    uint32_t sda0 = sd0 ^ sa11;
+    sd0 = st[b];
+    sa11 = st[c];
+    sda0 = sd0 ^ sa11;
     st[b] = Hacl_Impl_Chacha20_rotate_left(sda0, (uint32_t)12U);
-    uint32_t sa2 = st[a];
-    uint32_t sb2 = st[b];
+    sa2 = st[a];
+    sb2 = st[b];
     st[a] = sa2 + sb2;
-    uint32_t sd1 = st[d];
-    uint32_t sa12 = st[a];
-    uint32_t sda1 = sd1 ^ sa12;
+    sd1 = st[d];
+    sa12 = st[a];
+    sda1 = sd1 ^ sa12;
     st[d] = Hacl_Impl_Chacha20_rotate_left(sda1, (uint32_t)8U);
-    uint32_t sa3 = st[c];
-    uint32_t sb = st[d];
+    sa3 = st[c];
+    sb = st[d];
     st[c] = sa3 + sb;
-    uint32_t sd2 = st[b];
-    uint32_t sa1 = st[c];
-    uint32_t sda2 = sd2 ^ sa1;
+    sd2 = st[b];
+    sa1 = st[c];
+    sda2 = sd2 ^ sa1;
     st[b] = Hacl_Impl_Chacha20_rotate_left(sda2, (uint32_t)7U);
 }

@@ -90,14 +110,16 @@
 inline static void
 Hacl_Impl_Chacha20_rounds(uint32_t *st)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
         Hacl_Impl_Chacha20_double_round(st);
 }

 inline static void
 Hacl_Impl_Chacha20_sum_states(uint32_t *st, uint32_t *st_)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
         uint32_t xi = st[i];
         uint32_t yi = st_[i];
         st[i] = xi + yi;
@@ -150,9 +172,10 @@
     uint32_t *k = b;
     uint32_t *ib = b + (uint32_t)16U;
     uint32_t *ob = b + (uint32_t)32U;
+    uint32_t i;
     Hacl_Impl_Chacha20_chacha20_core(k, st, ctr);
     Hacl_Lib_LoadStore32_uint32s_from_le_bytes(ib, plain, (uint32_t)16U);
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
+    for (i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
         uint32_t xi = ib[i];
         uint32_t yi = k[i];
         ob[i] = xi ^ yi;
@@ -169,9 +192,11 @@
     uint32_t ctr)
 {
     uint8_t block[64U] = { 0U };
+    uint8_t *mask;
+    uint32_t i;
     Hacl_Impl_Chacha20_chacha20_block(block, st, ctr);
-    uint8_t *mask = block;
-    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+    mask = block;
+    for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
         uint8_t xi = plain[i];
         uint8_t yi = mask[i];
         output[i] = xi ^ yi;
@@ -186,7 +211,8 @@
     uint32_t *st,
     uint32_t ctr)
 {
-    for (uint32_t i = (uint32_t)0U; i < num_blocks; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < num_blocks; i = i + (uint32_t)1U) {
         uint8_t *b = plain + (uint32_t)64U * i;
         uint8_t *o = output + (uint32_t)64U * i;
         Hacl_Impl_Chacha20_update(o, b, st, ctr + i);
diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.h misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.h
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20.h	2018-10-21 21:12:36.078858000 -0700
@@ -13,6 +13,7 @@
  * limitations under the License.
  */

+#include "secport.h"
 #include "kremlib.h"
 #ifndef __Hacl_Chacha20_H
 #define __Hacl_Chacha20_H
diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c	2018-10-21 22:13:55.130785000 -0700
@@ -25,14 +25,18 @@
 inline static void
 Hacl_Impl_Chacha20_Vec128_State_state_to_key_block(uint8_t *stream_block, vec *k)
 {
+    uint8_t *a;
+    uint8_t *b;
+    uint8_t *c;
+    uint8_t *d;
     vec k0 = k[0U];
     vec k1 = k[1U];
     vec k2 = k[2U];
     vec k3 = k[3U];
-    uint8_t *a = stream_block;
-    uint8_t *b = stream_block + (uint32_t)16U;
-    uint8_t *c = stream_block + (uint32_t)32U;
-    uint8_t *d = stream_block + (uint32_t)48U;
+    a = stream_block;
+    b = stream_block + (uint32_t)16U;
+    c = stream_block + (uint32_t)32U;
+    d = stream_block + (uint32_t)48U;
     vec_store_le(a, k0);
     vec_store_le(b, k1);
     vec_store_le(c, k2);
@@ -42,21 +46,29 @@
 inline static void
 Hacl_Impl_Chacha20_Vec128_State_state_setup(vec *st, uint8_t *k, uint8_t *n1, uint32_t c)
 {
+    vec k0;
+    vec k1;
+    uint32_t n0;
+    uint8_t *x00;
+    uint32_t n10;
+    uint8_t *x0;
+    uint32_t n2;
+    vec v1;
     st[0U] =
         vec_load_32x4((uint32_t)0x61707865U,
                       (uint32_t)0x3320646eU,
                       (uint32_t)0x79622d32U,
                       (uint32_t)0x6b206574U);
-    vec k0 = vec_load128_le(k);
-    vec k1 = vec_load128_le(k + (uint32_t)16U);
+    k0 = vec_load128_le(k);
+    k1 = vec_load128_le(k + (uint32_t)16U);
     st[1U] = k0;
     st[2U] = k1;
-    uint32_t n0 = load32_le(n1);
-    uint8_t *x00 = n1 + (uint32_t)4U;
-    uint32_t n10 = load32_le(x00);
-    uint8_t *x0 = n1 + (uint32_t)8U;
-    uint32_t n2 = load32_le(x0);
-    vec v1 = vec_load_32x4(c, n0, n10, n2);
+    n0 = load32_le(n1);
+    x00 = n1 + (uint32_t)4U;
+    n10 = load32_le(x00);
+    x0 = n1 + (uint32_t)8U;
+    n2 = load32_le(x0);
+    v1 = vec_load_32x4(c, n0, n10, n2);
     st[3U] = v1;
 }

@@ -68,27 +80,42 @@
     vec sd0 = st[3U];
     vec sa10 = vec_add(sa, sb0);
     vec sd10 = vec_rotate_left(vec_xor(sd0, sa10), (uint32_t)16U);
+    vec sa0;
+    vec sb1;
+    vec sd2;
+    vec sa11;
+    vec sd11;
+    vec sa2;
+    vec sb2;
+    vec sd3;
+    vec sa12;
+    vec sd12;
+    vec sa3;
+    vec sb;
+    vec sd;
+    vec sa1;
+    vec sd1;
     st[0U] = sa10;
     st[3U] = sd10;
-    vec sa0 = st[2U];
-    vec sb1 = st[3U];
-    vec sd2 = st[1U];
-    vec sa11 = vec_add(sa0, sb1);
-    vec sd11 = vec_rotate_left(vec_xor(sd2, sa11), (uint32_t)12U);
+    sa0 = st[2U];
+    sb1 = st[3U];
+    sd2 = st[1U];
+    sa11 = vec_add(sa0, sb1);
+    sd11 = vec_rotate_left(vec_xor(sd2, sa11), (uint32_t)12U);
     st[2U] = sa11;
     st[1U] = sd11;
-    vec sa2 = st[0U];
-    vec sb2 = st[1U];
-    vec sd3 = st[3U];
-    vec sa12 = vec_add(sa2, sb2);
-    vec sd12 = vec_rotate_left(vec_xor(sd3, sa12), (uint32_t)8U);
+    sa2 = st[0U];
+    sb2 = st[1U];
+    sd3 = st[3U];
+    sa12 = vec_add(sa2, sb2);
+    sd12 = vec_rotate_left(vec_xor(sd3, sa12), (uint32_t)8U);
     st[0U] = sa12;
     st[3U] = sd12;
-    vec sa3 = st[2U];
-    vec sb = st[3U];
-    vec sd = st[1U];
-    vec sa1 = vec_add(sa3, sb);
-    vec sd1 = vec_rotate_left(vec_xor(sd, sa1), (uint32_t)7U);
+    sa3 = st[2U];
+    sb = st[3U];
+    sd = st[1U];
+    sa1 = vec_add(sa3, sb);
+    sd1 = vec_rotate_left(vec_xor(sd, sa1), (uint32_t)7U);
     st[2U] = sa1;
     st[1U] = sd1;
 }
@@ -96,17 +123,23 @@
 inline static void
 Hacl_Impl_Chacha20_Vec128_double_round(vec *st)
 {
+    vec r1;
+    vec r20;
+    vec r30;
+    vec r10;
+    vec r2;
+    vec r3;
     Hacl_Impl_Chacha20_Vec128_round(st);
-    vec r1 = st[1U];
-    vec r20 = st[2U];
-    vec r30 = st[3U];
+    r1 = st[1U];
+    r20 = st[2U];
+    r30 = st[3U];
     st[1U] = vec_shuffle_right(r1, (uint32_t)1U);
     st[2U] = vec_shuffle_right(r20, (uint32_t)2U);
     st[3U] = vec_shuffle_right(r30, (uint32_t)3U);
     Hacl_Impl_Chacha20_Vec128_round(st);
-    vec r10 = st[1U];
-    vec r2 = st[2U];
-    vec r3 = st[3U];
+    r10 = st[1U];
+    r2 = st[2U];
+    r3 = st[3U];
     st[1U] = vec_shuffle_right(r10, (uint32_t)3U);
     st[2U] = vec_shuffle_right(r2, (uint32_t)2U);
     st[3U] = vec_shuffle_right(r3, (uint32_t)1U);
@@ -153,8 +186,9 @@
 inline static void
 Hacl_Impl_Chacha20_Vec128_chacha20_core(vec *k, vec *st)
 {
+    uint32_t i;
     Hacl_Impl_Chacha20_Vec128_copy_state(k, st);
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
+    for (i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
         Hacl_Impl_Chacha20_Vec128_double_round(k);
     Hacl_Impl_Chacha20_Vec128_sum_states(k, st);
 }
@@ -188,8 +222,9 @@
 inline static void
 Hacl_Impl_Chacha20_Vec128_chacha20_core3(vec *k0, vec *k1, vec *k2, vec *st)
 {
+    uint32_t i;
     Hacl_Impl_Chacha20_Vec128_chacha20_incr3(k0, k1, k2, st);
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
+    for (i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
         Hacl_Impl_Chacha20_Vec128_double_round3(k0, k1, k2);
     Hacl_Impl_Chacha20_Vec128_chacha20_sum3(k0, k1, k2, st);
 }
@@ -197,9 +232,10 @@
 inline static void
 Hacl_Impl_Chacha20_Vec128_chacha20_block(uint8_t *stream_block, vec *st)
 {
-    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
     vec k[4U];
-    for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
+    uint32_t _i;
+    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
+    for (_i = 0U; _i < (uint32_t)4U; ++_i)
         k[_i] = vec_zero();
     Hacl_Impl_Chacha20_Vec128_chacha20_core(k, st);
     Hacl_Impl_Chacha20_Vec128_State_state_to_key_block(stream_block, k);
@@ -215,9 +251,11 @@
 Hacl_Impl_Chacha20_Vec128_update_last(uint8_t *output, uint8_t *plain, uint32_t len, vec *st)
 {
     uint8_t block[64U] = { 0U };
+    uint8_t *mask;
+    uint32_t i;
     Hacl_Impl_Chacha20_Vec128_chacha20_block(block, st);
-    uint8_t *mask = block;
-    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+    mask = block;
+    for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
         uint8_t xi = plain[i];
         uint8_t yi = mask[i];
         output[i] = xi ^ yi;
@@ -252,9 +290,10 @@
 static void
 Hacl_Impl_Chacha20_Vec128_update(uint8_t *output, uint8_t *plain, vec *st)
 {
-    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
     vec k[4U];
-    for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
+    uint32_t _i;
+    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
+    for (_i = 0U; _i < (uint32_t)4U; ++_i)
         k[_i] = vec_zero();
     Hacl_Impl_Chacha20_Vec128_chacha20_core(k, st);
     Hacl_Impl_Chacha20_Vec128_xor_block(output, plain, k);
@@ -263,25 +302,32 @@
 static void
 Hacl_Impl_Chacha20_Vec128_update3(uint8_t *output, uint8_t *plain, vec *st)
 {
-    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
     vec k0[4U];
-    for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
+    uint32_t _i;
+    vec k1[4U];
+    vec k2[4U];
+    uint8_t *p0;
+    uint8_t *p1;
+    uint8_t *p2;
+    uint8_t *o0;
+    uint8_t *o1;
+    uint8_t *o2;
+    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
+    for (_i = 0U; _i < (uint32_t)4U; ++_i)
         k0[_i] = vec_zero();
     KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
-    vec k1[4U];
-    for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
+    for (_i = 0U; _i < (uint32_t)4U; ++_i)
         k1[_i] = vec_zero();
     KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
-    vec k2[4U];
-    for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
+    for (_i = 0U; _i < (uint32_t)4U; ++_i)
         k2[_i] = vec_zero();
     Hacl_Impl_Chacha20_Vec128_chacha20_core3(k0, k1, k2, st);
-    uint8_t *p0 = plain;
-    uint8_t *p1 = plain + (uint32_t)64U;
-    uint8_t *p2 = plain + (uint32_t)128U;
-    uint8_t *o0 = output;
-    uint8_t *o1 = output + (uint32_t)64U;
-    uint8_t *o2 = output + (uint32_t)128U;
+    p0 = plain;
+    p1 = plain + (uint32_t)64U;
+    p2 = plain + (uint32_t)128U;
+    o0 = output;
+    o1 = output + (uint32_t)64U;
+    o2 = output + (uint32_t)128U;
     Hacl_Impl_Chacha20_Vec128_xor_block(o0, p0, k0);
     Hacl_Impl_Chacha20_Vec128_xor_block(o1, p1, k1);
     Hacl_Impl_Chacha20_Vec128_xor_block(o2, p2, k2);
@@ -308,7 +354,8 @@
     uint32_t len,
     vec *st)
 {
-    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U)
+    uint32_t i;
+    for (i = (uint32_t)0U; i < len; i = i + (uint32_t)1U)
         Hacl_Impl_Chacha20_Vec128_update3_(output, plain, len, st, i);
 }

@@ -368,11 +415,13 @@
     uint8_t *n1,
     uint32_t ctr)
 {
-    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
     vec buf[4U];
-    for (uint32_t _i = 0U; _i < (uint32_t)4U; ++_i)
+    uint32_t _i;
+    vec *st;
+    KRML_CHECK_SIZE(vec_zero(), (uint32_t)4U);
+    for (_i = 0U; _i < (uint32_t)4U; ++_i)
         buf[_i] = vec_zero();
-    vec *st = buf;
+    st = buf;
     Hacl_Impl_Chacha20_Vec128_init(st, k, n1, ctr);
     Hacl_Impl_Chacha20_Vec128_chacha20_counter_mode(output, plain, len, st);
 }
diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.h misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.h
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.h	2018-10-21 21:52:15.090683000 -0700
@@ -13,6 +13,7 @@
  * limitations under the License.
  */

+#include "secport.h"
 #include "kremlib.h"
 #ifndef __Hacl_Chacha20_Vec128_H
 #define __Hacl_Chacha20_Vec128_H
diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.c misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.c
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.c	2018-10-21 22:57:57.044565000 -0700
@@ -129,6 +129,7 @@
 Hacl_Bignum_Fmul_shift_reduce(uint64_t *output)
 {
     uint64_t tmp = output[4U];
+    uint64_t b0;
     {
         uint32_t ctr = (uint32_t)5U - (uint32_t)0U - (uint32_t)1U;
         uint64_t z = output[ctr - (uint32_t)1U];
@@ -150,13 +151,15 @@
         output[ctr] = z;
     }
     output[0U] = tmp;
-    uint64_t b0 = output[0U];
+    b0 = output[0U];
     output[0U] = (uint64_t)19U * b0;
 }

 static void
 Hacl_Bignum_Fmul_mul_shift_reduce_(FStar_UInt128_t *output, uint64_t *input, uint64_t *input21)
 {
+    uint32_t i;
+    uint64_t input2i;
     {
         uint64_t input2i = input21[0U];
         Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
@@ -177,8 +180,8 @@
         Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
         Hacl_Bignum_Fmul_shift_reduce(input);
     }
-    uint32_t i = (uint32_t)4U;
-    uint64_t input2i = input21[i];
+    i = (uint32_t)4U;
+    input2i = input21[i];
     Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
 }

@@ -186,29 +189,35 @@
 Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input21)
 {
     uint64_t tmp[5U] = { 0U };
+    uint32_t _i;
+    FStar_UInt128_t b4;
+    FStar_UInt128_t b0;
+    FStar_UInt128_t b4_;
+    FStar_UInt128_t b0_;
+    FStar_UInt128_t t[5U];
+    uint64_t i0;
+    uint64_t i1;
+    uint64_t i0_;
+    uint64_t i1_;
     memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
     KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
-    FStar_UInt128_t t[5U];
-    for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
+    for (_i = 0U; _i < (uint32_t)5U; ++_i)
         t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
     Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input21);
     Hacl_Bignum_Fproduct_carry_wide_(t);
-    FStar_UInt128_t b4 = t[4U];
-    FStar_UInt128_t b0 = t[0U];
-    FStar_UInt128_t
-        b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
-    FStar_UInt128_t
-        b0_ =
-            FStar_UInt128_add(b0,
+    b4 = t[4U];
+    b0 = t[0U];
+    b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
+    b0_ = FStar_UInt128_add(b0,
                               FStar_UInt128_mul_wide((uint64_t)19U,
                                                      FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
     t[4U] = b4_;
     t[0U] = b0_;
     Hacl_Bignum_Fproduct_copy_from_wide_(output, t);
-    uint64_t i0 = output[0U];
-    uint64_t i1 = output[1U];
-    uint64_t i0_ = i0 & (uint64_t)0x7ffffffffffffU;
-    uint64_t i1_ = i1 + (i0 >> (uint32_t)51U);
+    i0 = output[0U];
+    i1 = output[1U];
+    i0_ = i0 & (uint64_t)0x7ffffffffffffU;
+    i1_ = i1 + (i0 >> (uint32_t)51U);
     output[0U] = i0_;
     output[1U] = i1_;
 }
@@ -226,28 +235,28 @@
     uint64_t d2 = r2 * (uint64_t)2U * (uint64_t)19U;
     uint64_t d419 = r4 * (uint64_t)19U;
     uint64_t d4 = d419 * (uint64_t)2U;
-    FStar_UInt128_t
-        s0 =
+    FStar_UInt128_t s0;
+    FStar_UInt128_t s1;
+    FStar_UInt128_t s2;
+    FStar_UInt128_t s3;
+    FStar_UInt128_t s4;
+    s0 =
             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(r0, r0),
                                                 FStar_UInt128_mul_wide(d4, r1)),
                               FStar_UInt128_mul_wide(d2, r3));
-    FStar_UInt128_t
-        s1 =
+    s1 =
             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r1),
                                                 FStar_UInt128_mul_wide(d4, r2)),
                               FStar_UInt128_mul_wide(r3 * (uint64_t)19U, r3));
-    FStar_UInt128_t
-        s2 =
+    s2 =
             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r2),
                                                 FStar_UInt128_mul_wide(r1, r1)),
                               FStar_UInt128_mul_wide(d4, r3));
-    FStar_UInt128_t
-        s3 =
+    s3 =
             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r3),
                                                 FStar_UInt128_mul_wide(d1, r2)),
                               FStar_UInt128_mul_wide(r4, d419));
-    FStar_UInt128_t
-        s4 =
+    s4 =
             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r4),
                                                 FStar_UInt128_mul_wide(d1, r3)),
                               FStar_UInt128_mul_wide(r2, r2));
@@ -261,24 +270,30 @@
 inline static void
 Hacl_Bignum_Fsquare_fsquare_(FStar_UInt128_t *tmp, uint64_t *output)
 {
+    FStar_UInt128_t b4;
+    FStar_UInt128_t b0;
+    FStar_UInt128_t b4_;
+    FStar_UInt128_t b0_;
+    uint64_t i0;
+    uint64_t i1;
+    uint64_t i0_;
+    uint64_t i1_;
     Hacl_Bignum_Fsquare_fsquare__(tmp, output);
     Hacl_Bignum_Fproduct_carry_wide_(tmp);
-    FStar_UInt128_t b4 = tmp[4U];
-    FStar_UInt128_t b0 = tmp[0U];
-    FStar_UInt128_t
-        b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
-    FStar_UInt128_t
-        b0_ =
+    b4 = tmp[4U];
+    b0 = tmp[0U];
+    b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
+    b0_ =
             FStar_UInt128_add(b0,
                               FStar_UInt128_mul_wide((uint64_t)19U,
                                                      FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
     tmp[4U] = b4_;
     tmp[0U] = b0_;
     Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);
-    uint64_t i0 = output[0U];
-    uint64_t i1 = output[1U];
-    uint64_t i0_ = i0 & (uint64_t)0x7ffffffffffffU;
-    uint64_t i1_ = i1 + (i0 >> (uint32_t)51U);
+    i0 = output[0U];
+    i1 = output[1U];
+    i0_ = i0 & (uint64_t)0x7ffffffffffffU;
+    i1_ = i1 + (i0 >> (uint32_t)51U);
     output[0U] = i0_;
     output[1U] = i1_;
 }
@@ -286,17 +301,19 @@
 static void
 Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, FStar_UInt128_t *tmp, uint32_t count1)
 {
+    uint32_t i;
     Hacl_Bignum_Fsquare_fsquare_(tmp, input);
-    for (uint32_t i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U)
+    for (i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U)
         Hacl_Bignum_Fsquare_fsquare_(tmp, input);
 }

 inline static void
 Hacl_Bignum_Fsquare_fsquare_times(uint64_t *output, uint64_t *input, uint32_t count1)
 {
-    KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
     FStar_UInt128_t t[5U];
-    for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
+    uint32_t _i;
+    KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
+    for (_i = 0U; _i < (uint32_t)5U; ++_i)
         t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
     memcpy(output, input, (uint32_t)5U * sizeof input[0U]);
     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);
@@ -305,9 +322,10 @@
 inline static void
 Hacl_Bignum_Fsquare_fsquare_times_inplace(uint64_t *output, uint32_t count1)
 {
-    KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
     FStar_UInt128_t t[5U];
-    for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
+    uint32_t _i;
+    KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
+    for (_i = 0U; _i < (uint32_t)5U; ++_i)
         t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
     Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1);
 }
@@ -319,6 +337,13 @@
     uint64_t *a = buf;
     uint64_t *t00 = buf + (uint32_t)5U;
     uint64_t *b0 = buf + (uint32_t)10U;
+    uint64_t *t01;
+    uint64_t *b1;
+    uint64_t *c0;
+    uint64_t *a0;
+    uint64_t *t0;
+    uint64_t *b;
+    uint64_t *c;
     Hacl_Bignum_Fsquare_fsquare_times(a, z, (uint32_t)1U);
     Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)2U);
     Hacl_Bignum_Fmul_fmul(b0, t00, z);
@@ -326,9 +351,9 @@
     Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)1U);
     Hacl_Bignum_Fmul_fmul(b0, t00, b0);
     Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U);
-    uint64_t *t01 = buf + (uint32_t)5U;
-    uint64_t *b1 = buf + (uint32_t)10U;
-    uint64_t *c0 = buf + (uint32_t)15U;
+    t01 = buf + (uint32_t)5U;
+    b1 = buf + (uint32_t)10U;
+    c0 = buf + (uint32_t)15U;
     Hacl_Bignum_Fmul_fmul(b1, t01, b1);
     Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U);
     Hacl_Bignum_Fmul_fmul(c0, t01, b1);
@@ -337,10 +362,10 @@
     Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U);
     Hacl_Bignum_Fmul_fmul(b1, t01, b1);
     Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U);
-    uint64_t *a0 = buf;
-    uint64_t *t0 = buf + (uint32_t)5U;
-    uint64_t *b = buf + (uint32_t)10U;
-    uint64_t *c = buf + (uint32_t)15U;
+    a0 = buf;
+    t0 = buf + (uint32_t)5U;
+    b = buf + (uint32_t)10U;
+    c = buf + (uint32_t)15U;
     Hacl_Bignum_Fmul_fmul(c, t0, b);
     Hacl_Bignum_Fsquare_fsquare_times(t0, c, (uint32_t)100U);
     Hacl_Bignum_Fmul_fmul(t0, t0, c);
@@ -384,12 +409,17 @@
 Hacl_Bignum_fdifference(uint64_t *a, uint64_t *b)
 {
     uint64_t tmp[5U] = { 0U };
+    uint64_t b0;
+    uint64_t b1;
+    uint64_t b2;
+    uint64_t b3;
+    uint64_t b4;
     memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]);
-    uint64_t b0 = tmp[0U];
-    uint64_t b1 = tmp[1U];
-    uint64_t b2 = tmp[2U];
-    uint64_t b3 = tmp[3U];
-    uint64_t b4 = tmp[4U];
+    b0 = tmp[0U];
+    b1 = tmp[1U];
+    b2 = tmp[2U];
+    b3 = tmp[3U];
+    b4 = tmp[4U];
     tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U;
     tmp[1U] = b1 + (uint64_t)0x3ffffffffffff8U;
     tmp[2U] = b2 + (uint64_t)0x3ffffffffffff8U;
@@ -425,9 +455,14 @@
 inline static void
 Hacl_Bignum_fscalar(uint64_t *output, uint64_t *b, uint64_t s)
 {
-    KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
     FStar_UInt128_t tmp[5U];
-    for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
+    uint32_t _i;
+    FStar_UInt128_t b4;
+    FStar_UInt128_t b0;
+    FStar_UInt128_t b4_;
+    FStar_UInt128_t b0_;
+    KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U);
+    for (_i = 0U; _i < (uint32_t)5U; ++_i)
         tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
     {
         uint64_t xi = b[0U];
@@ -450,12 +485,10 @@
         tmp[4U] = FStar_UInt128_mul_wide(xi, s);
     }
     Hacl_Bignum_Fproduct_carry_wide_(tmp);
-    FStar_UInt128_t b4 = tmp[4U];
-    FStar_UInt128_t b0 = tmp[0U];
-    FStar_UInt128_t
-        b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
-    FStar_UInt128_t
-        b0_ =
+    b4 = tmp[4U];
+    b0 = tmp[0U];
+    b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU));
+    b0_ =
             FStar_UInt128_add(b0,
                               FStar_UInt128_mul_wide((uint64_t)19U,
                                                      FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U))));
@@ -492,9 +525,10 @@
 static void
 Hacl_EC_Point_swap_conditional_(uint64_t *a, uint64_t *b, uint64_t swap1, uint32_t ctr)
 {
+    uint32_t i;
     if (!(ctr == (uint32_t)0U)) {
         Hacl_EC_Point_swap_conditional_step(a, b, swap1, ctr);
-        uint32_t i = ctr - (uint32_t)1U;
+        i = ctr - (uint32_t)1U;
         Hacl_EC_Point_swap_conditional_(a, b, swap1, i);
     }
 }
@@ -538,6 +572,16 @@
     uint64_t *origxprime = buf + (uint32_t)5U;
     uint64_t *xxprime0 = buf + (uint32_t)25U;
     uint64_t *zzprime0 = buf + (uint32_t)30U;
+    uint64_t *origxprime0;
+    uint64_t *xx0;
+    uint64_t *zz0;
+    uint64_t *xxprime;
+    uint64_t *zzprime;
+    uint64_t *zzzprime;
+    uint64_t *zzz;
+    uint64_t *xx;
+    uint64_t *zz;
+    uint64_t scalar = (uint64_t)121665U;
     memcpy(origx, x, (uint32_t)5U * sizeof x[0U]);
     Hacl_Bignum_fsum(x, z);
     Hacl_Bignum_fdifference(z, origx);
@@ -546,12 +590,12 @@
     Hacl_Bignum_fdifference(zprime, origxprime);
     Hacl_Bignum_fmul(xxprime0, xprime, z);
     Hacl_Bignum_fmul(zzprime0, x, zprime);
-    uint64_t *origxprime0 = buf + (uint32_t)5U;
-    uint64_t *xx0 = buf + (uint32_t)15U;
-    uint64_t *zz0 = buf + (uint32_t)20U;
-    uint64_t *xxprime = buf + (uint32_t)25U;
-    uint64_t *zzprime = buf + (uint32_t)30U;
-    uint64_t *zzzprime = buf + (uint32_t)35U;
+    origxprime0 = buf + (uint32_t)5U;
+    xx0 = buf + (uint32_t)15U;
+    zz0 = buf + (uint32_t)20U;
+    xxprime = buf + (uint32_t)25U;
+    zzprime = buf + (uint32_t)30U;
+    zzzprime = buf + (uint32_t)35U;
     memcpy(origxprime0, xxprime, (uint32_t)5U * sizeof xxprime[0U]);
     Hacl_Bignum_fsum(xxprime, zzprime);
     Hacl_Bignum_fdifference(zzprime, origxprime0);
@@ -560,12 +604,11 @@
     Hacl_Bignum_fmul(z3, zzzprime, qx);
     Hacl_Bignum_Fsquare_fsquare_times(xx0, x, (uint32_t)1U);
     Hacl_Bignum_Fsquare_fsquare_times(zz0, z, (uint32_t)1U);
-    uint64_t *zzz = buf + (uint32_t)10U;
-    uint64_t *xx = buf + (uint32_t)15U;
-    uint64_t *zz = buf + (uint32_t)20U;
+    zzz = buf + (uint32_t)10U;
+    xx = buf + (uint32_t)15U;
+    zz = buf + (uint32_t)20U;
     Hacl_Bignum_fmul(x2, xx, zz);
     Hacl_Bignum_fdifference(zz, xx);
-    uint64_t scalar = (uint64_t)121665U;
     Hacl_Bignum_fscalar(zzz, zz, scalar);
     Hacl_Bignum_fsum(zzz, xx);
     Hacl_Bignum_fmul(z2, zzz, zz);
@@ -581,9 +624,10 @@
     uint8_t byt)
 {
     uint64_t bit = (uint64_t)(byt >> (uint32_t)7U);
+    uint64_t bit0;
     Hacl_EC_Point_swap_conditional(nq, nqpq, bit);
     Hacl_EC_AddAndDouble_fmonty(nq2, nqpq2, nq, nqpq, q);
-    uint64_t bit0 = (uint64_t)(byt >> (uint32_t)7U);
+    bit0 = (uint64_t)(byt >> (uint32_t)7U);
     Hacl_EC_Point_swap_conditional(nq2, nqpq2, bit0);
 }

@@ -596,8 +640,9 @@
     uint64_t *q,
     uint8_t byt)
 {
+    uint8_t byt1;
     Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step(nq, nqpq, nq2, nqpq2, q, byt);
-    uint8_t byt1 = byt << (uint32_t)1U;
+    byt1 = byt << (uint32_t)1U;
     Hacl_EC_Ladder_SmallLoop_cmult_small_loop_step(nq2, nqpq2, nq, nqpq, q, byt1);
 }

@@ -613,8 +658,9 @@
 {
     if (!(i == (uint32_t)0U)) {
         uint32_t i_ = i - (uint32_t)1U;
+        uint8_t byt_;
         Hacl_EC_Ladder_SmallLoop_cmult_small_loop_double_step(nq, nqpq, nq2, nqpq2, q, byt);
-        uint8_t byt_ = byt << (uint32_t)2U;
+        byt_ = byt << (uint32_t)2U;
         Hacl_EC_Ladder_SmallLoop_cmult_small_loop(nq, nqpq, nq2, nqpq2, q, byt_, i_);
     }
 }
@@ -731,12 +777,16 @@
 static void
 Hacl_EC_Format_fcontract_second_carry_full(uint64_t *input)
 {
+    uint64_t i0;
+    uint64_t i1;
+    uint64_t i0_;
+    uint64_t i1_;
     Hacl_EC_Format_fcontract_second_carry_pass(input);
     Hacl_Bignum_Modulo_carry_top(input);
-    uint64_t i0 = input[0U];
-    uint64_t i1 = input[1U];
-    uint64_t i0_ = i0 & (uint64_t)0x7ffffffffffffU;
-    uint64_t i1_ = i1 + (i0 >> (uint32_t)51U);
+    i0 = input[0U];
+    i1 = input[1U];
+    i0_ = i0 & (uint64_t)0x7ffffffffffffU;
+    i1_ = i1 + (i0 >> (uint32_t)51U);
     input[0U] = i0_;
     input[1U] = i1_;
 }
@@ -817,22 +867,31 @@
     uint64_t buf0[10U] = { 0U };
     uint64_t *x0 = buf0;
     uint64_t *z = buf0 + (uint32_t)5U;
+    uint64_t *q;
+    uint8_t e[32U] = { 0U };
+    uint8_t e0;
+    uint8_t e31;
+    uint8_t e01;
+    uint8_t e311;
+    uint8_t e312;
+    uint8_t *scalar;
+    uint64_t buf[15U] = { 0U };
+    uint64_t *nq;
+    uint64_t *x;
     Hacl_EC_Format_fexpand(x0, basepoint);
     z[0U] = (uint64_t)1U;
-    uint64_t *q = buf0;
-    uint8_t e[32U] = { 0U };
+    q = buf0;
     memcpy(e, secret, (uint32_t)32U * sizeof secret[0U]);
-    uint8_t e0 = e[0U];
-    uint8_t e31 = e[31U];
-    uint8_t e01 = e0 & (uint8_t)248U;
-    uint8_t e311 = e31 & (uint8_t)127U;
-    uint8_t e312 = e311 | (uint8_t)64U;
+    e0 = e[0U];
+    e31 = e[31U];
+    e01 = e0 & (uint8_t)248U;
+    e311 = e31 & (uint8_t)127U;
+    e312 = e311 | (uint8_t)64U;
     e[0U] = e01;
     e[31U] = e312;
-    uint8_t *scalar = e;
-    uint64_t buf[15U] = { 0U };
-    uint64_t *nq = buf;
-    uint64_t *x = nq;
+    scalar = e;
+    nq = buf;
+    x = nq;
     x[0U] = (uint64_t)1U;
     Hacl_EC_Ladder_cmult(nq, scalar, q);
     Hacl_EC_Format_scalar_of_point(mypublic, nq);
diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.h misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.h
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Curve25519.h	2018-10-21 22:18:23.286647000 -0700
@@ -13,6 +13,7 @@
  * limitations under the License.
  */

+#include "secport.h"
 #include "kremlib.h"
 #ifndef __Hacl_Curve25519_H
 #define __Hacl_Curve25519_H
diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.c misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.c
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.c	2018-10-22 00:58:55.601973000 -0700
@@ -47,7 +47,8 @@
 inline static void
 Hacl_Bignum_Fproduct_copy_from_wide_(uint32_t *output, uint64_t *input)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
         uint64_t xi = input[i];
         output[i] = (uint32_t)xi;
     }
@@ -56,7 +57,8 @@
 inline static void
 Hacl_Bignum_Fproduct_sum_scalar_multiplication_(uint64_t *output, uint32_t *input, uint32_t s)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
         uint64_t xi = output[i];
         uint32_t yi = input[i];
         uint64_t x_wide = (uint64_t)yi;
@@ -68,7 +70,8 @@
 inline static void
 Hacl_Bignum_Fproduct_carry_wide_(uint64_t *tmp)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
         uint32_t ctr = i;
         uint64_t tctr = tmp[ctr];
         uint64_t tctrp1 = tmp[ctr + (uint32_t)1U];
@@ -82,7 +85,8 @@
 inline static void
 Hacl_Bignum_Fproduct_carry_limb_(uint32_t *tmp)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
         uint32_t ctr = i;
         uint32_t tctr = tmp[ctr];
         uint32_t tctrp1 = tmp[ctr + (uint32_t)1U];
@@ -97,7 +101,8 @@
 Hacl_Bignum_Fmul_shift_reduce(uint32_t *output)
 {
     uint32_t tmp = output[4U];
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
         uint32_t ctr = (uint32_t)5U - i - (uint32_t)1U;
         uint32_t z = output[ctr - (uint32_t)1U];
         output[ctr] = z;
@@ -109,13 +114,15 @@
 static void
 Hacl_Bignum_Fmul_mul_shift_reduce_(uint64_t *output, uint32_t *input, uint32_t *input2)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    uint32_t input2i;
+    for (i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
         uint32_t input2i = input2[i];
         Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
         Hacl_Bignum_Fmul_shift_reduce(input);
     }
-    uint32_t i = (uint32_t)4U;
-    uint32_t input2i = input2[i];
+    i = (uint32_t)4U;
+    input2i = input2[i];
     Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
 }

@@ -123,16 +130,20 @@
 Hacl_Bignum_Fmul_fmul(uint32_t *output, uint32_t *input, uint32_t *input2)
 {
     uint32_t tmp[5U] = { 0U };
-    memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
     uint64_t t[5U] = { 0U };
+    uint32_t i0;
+    uint32_t i1;
+    uint32_t i0_;
+    uint32_t i1_;
+    memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
     Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input2);
     Hacl_Bignum_Fproduct_carry_wide_(t);
     Hacl_Bignum_Modulo_carry_top_wide(t);
     Hacl_Bignum_Fproduct_copy_from_wide_(output, t);
-    uint32_t i0 = output[0U];
-    uint32_t i1 = output[1U];
-    uint32_t i0_ = i0 & (uint32_t)0x3ffffffU;
-    uint32_t i1_ = i1 + (i0 >> (uint32_t)26U);
+    i0 = output[0U];
+    i1 = output[1U];
+    i0_ = i0 & (uint32_t)0x3ffffffU;
+    i1_ = i1 + (i0 >> (uint32_t)26U);
     output[0U] = i0_;
     output[1U] = i1_;
 }
@@ -140,7 +151,8 @@
 inline static void
 Hacl_Bignum_AddAndMultiply_add_and_multiply(uint32_t *acc, uint32_t *block, uint32_t *r)
 {
-    for (uint32_t i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
+    uint32_t i;
+    for (i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
         uint32_t xi = acc[i];
         uint32_t yi = block[i];
         acc[i] = xi + yi;
@@ -175,13 +187,15 @@
     uint32_t r2 = i2 >> (uint32_t)4U & (uint32_t)0x3ffffffU;
     uint32_t r3 = i3 >> (uint32_t)6U & (uint32_t)0x3ffffffU;
     uint32_t r4 = i4 >> (uint32_t)8U;
+    uint32_t b4;
+    uint32_t b4_;
     tmp[0U] = r0;
     tmp[1U] = r1;
     tmp[2U] = r2;
     tmp[3U] = r3;
     tmp[4U] = r4;
-    uint32_t b4 = tmp[4U];
-    uint32_t b4_ = (uint32_t)0x1000000U | b4;
+    b4 = tmp[4U];
+    b4_ = (uint32_t)0x1000000U | b4;
     tmp[4U] = b4_;
     Hacl_Bignum_AddAndMultiply_add_and_multiply(acc, tmp, r5);
 }
@@ -209,15 +223,19 @@
     uint32_t r2 = i2 >> (uint32_t)4U & (uint32_t)0x3ffffffU;
     uint32_t r3 = i3 >> (uint32_t)6U & (uint32_t)0x3ffffffU;
     uint32_t r4 = i4 >> (uint32_t)8U;
+    Hacl_Impl_Poly1305_32_State_poly1305_state scrut0;
+    uint32_t *h;
+    Hacl_Impl_Poly1305_32_State_poly1305_state scrut;
+    uint32_t *r;
     tmp[0U] = r0;
     tmp[1U] = r1;
     tmp[2U] = r2;
     tmp[3U] = r3;
     tmp[4U] = r4;
-    Hacl_Impl_Poly1305_32_State_poly1305_state scrut0 = st;
-    uint32_t *h = scrut0.h;
-    Hacl_Impl_Poly1305_32_State_poly1305_state scrut = st;
-    uint32_t *r = scrut.r;
+    scrut0 = st;
+    h = scrut0.h;
+    scrut = st;
+    r = scrut.r;
     Hacl_Bignum_AddAndMultiply_add_and_multiply(h, tmp, r);
 }

@@ -228,12 +246,15 @@
     uint64_t rem_)
 {
     uint8_t zero1 = (uint8_t)0U;
-    KRML_CHECK_SIZE(zero1, (uint32_t)16U);
     uint8_t block[16U];
-    for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
+    uint32_t _i;
+    uint32_t i0;
+    uint32_t i;
+    KRML_CHECK_SIZE(zero1, (uint32_t)16U);
+    for (_i = 0U; _i < (uint32_t)16U; ++_i)
         block[_i] = zero1;
-    uint32_t i0 = (uint32_t)rem_;
-    uint32_t i = (uint32_t)rem_;
+    i0 = (uint32_t)rem_;
+    i = (uint32_t)rem_;
     memcpy(block, m, i * sizeof m[0U]);
     block[i0] = (uint8_t)1U;
     Hacl_Impl_Poly1305_32_poly1305_process_last_block_(block, st, m, rem_);
@@ -242,69 +263,116 @@
 static void
 Hacl_Impl_Poly1305_32_poly1305_last_pass(uint32_t *acc)
 {
+    uint32_t t0;
+    uint32_t t10;
+    uint32_t t20;
+    uint32_t t30;
+    uint32_t t40;
+    uint32_t t1_;
+    uint32_t mask_261;
+    uint32_t t0_;
+    uint32_t t2_;
+    uint32_t t1__;
+    uint32_t t3_;
+    uint32_t t2__;
+    uint32_t t4_;
+    uint32_t t3__;
+    uint32_t t00;
+    uint32_t t1;
+    uint32_t t2;
+    uint32_t t3;
+    uint32_t t4;
+    uint32_t t1_0;
+    uint32_t t0_0;
+    uint32_t t2_0;
+    uint32_t t1__0;
+    uint32_t t3_0;
+    uint32_t t2__0;
+    uint32_t t4_0;
+    uint32_t t3__0;
+    uint32_t i0;
+    uint32_t i1;
+    uint32_t i0_;
+    uint32_t i1_;
+    uint32_t a0;
+    uint32_t a1;
+    uint32_t a2;
+    uint32_t a3;
+    uint32_t a4;
+    uint32_t mask0;
+    uint32_t mask1;
+    uint32_t mask2;
+    uint32_t mask3;
+    uint32_t mask4;
+    uint32_t mask;
+    uint32_t a0_;
+    uint32_t a1_;
+    uint32_t a2_;
+    uint32_t a3_;
+    uint32_t a4_;
     Hacl_Bignum_Fproduct_carry_limb_(acc);
     Hacl_Bignum_Modulo_carry_top(acc);
-    uint32_t t0 = acc[0U];
-    uint32_t t10 = acc[1U];
-    uint32_t t20 = acc[2U];
-    uint32_t t30 = acc[3U];
-    uint32_t t40 = acc[4U];
-    uint32_t t1_ = t10 + (t0 >> (uint32_t)26U);
-    uint32_t mask_261 = (uint32_t)0x3ffffffU;
-    uint32_t t0_ = t0 & mask_261;
-    uint32_t t2_ = t20 + (t1_ >> (uint32_t)26U);
-    uint32_t t1__ = t1_ & mask_261;
-    uint32_t t3_ = t30 + (t2_ >> (uint32_t)26U);
-    uint32_t t2__ = t2_ & mask_261;
-    uint32_t t4_ = t40 + (t3_ >> (uint32_t)26U);
-    uint32_t t3__ = t3_ & mask_261;
+    t0 = acc[0U];
+    t10 = acc[1U];
+    t20 = acc[2U];
+    t30 = acc[3U];
+    t40 = acc[4U];
+    t1_ = t10 + (t0 >> (uint32_t)26U);
+    mask_261 = (uint32_t)0x3ffffffU;
+    t0_ = t0 & mask_261;
+    t2_ = t20 + (t1_ >> (uint32_t)26U);
+    t1__ = t1_ & mask_261;
+    t3_ = t30 + (t2_ >> (uint32_t)26U);
+    t2__ = t2_ & mask_261;
+    t4_ = t40 + (t3_ >> (uint32_t)26U);
+    t3__ = t3_ & mask_261;
     acc[0U] = t0_;
     acc[1U] = t1__;
     acc[2U] = t2__;
     acc[3U] = t3__;
     acc[4U] = t4_;
     Hacl_Bignum_Modulo_carry_top(acc);
-    uint32_t t00 = acc[0U];
-    uint32_t t1 = acc[1U];
-    uint32_t t2 = acc[2U];
-    uint32_t t3 = acc[3U];
-    uint32_t t4 = acc[4U];
-    uint32_t t1_0 = t1 + (t00 >> (uint32_t)26U);
-    uint32_t t0_0 = t00 & (uint32_t)0x3ffffffU;
-    uint32_t t2_0 = t2 + (t1_0 >> (uint32_t)26U);
-    uint32_t t1__0 = t1_0 & (uint32_t)0x3ffffffU;
-    uint32_t t3_0 = t3 + (t2_0 >> (uint32_t)26U);
-    uint32_t t2__0 = t2_0 & (uint32_t)0x3ffffffU;
-    uint32_t t4_0 = t4 + (t3_0 >> (uint32_t)26U);
-    uint32_t t3__0 = t3_0 & (uint32_t)0x3ffffffU;
+    t00 = acc[0U];
+    t1 = acc[1U];
+    t2 = acc[2U];
+    t3 = acc[3U];
+    t4 = acc[4U];
+    t1_0 = t1 + (t00 >> (uint32_t)26U);
+    t0_0 = t00 & (uint32_t)0x3ffffffU;
+    t2_0 = t2 + (t1_0 >> (uint32_t)26U);
+    t1__0 = t1_0 & (uint32_t)0x3ffffffU;
+    t3_0 = t3 + (t2_0 >> (uint32_t)26U);
+    t2__0 = t2_0 & (uint32_t)0x3ffffffU;
+    t4_0 = t4 + (t3_0 >> (uint32_t)26U);
+    t3__0 = t3_0 & (uint32_t)0x3ffffffU;
     acc[0U] = t0_0;
     acc[1U] = t1__0;
     acc[2U] = t2__0;
     acc[3U] = t3__0;
     acc[4U] = t4_0;
     Hacl_Bignum_Modulo_carry_top(acc);
-    uint32_t i0 = acc[0U];
-    uint32_t i1 = acc[1U];
-    uint32_t i0_ = i0 & (uint32_t)0x3ffffffU;
-    uint32_t i1_ = i1 + (i0 >> (uint32_t)26U);
+    i0 = acc[0U];
+    i1 = acc[1U];
+    i0_ = i0 & (uint32_t)0x3ffffffU;
+    i1_ = i1 + (i0 >> (uint32_t)26U);
     acc[0U] = i0_;
     acc[1U] = i1_;
-    uint32_t a0 = acc[0U];
-    uint32_t a1 = acc[1U];
-    uint32_t a2 = acc[2U];
-    uint32_t a3 = acc[3U];
-    uint32_t a4 = acc[4U];
-    uint32_t mask0 = FStar_UInt32_gte_mask(a0, (uint32_t)0x3fffffbU);
-    uint32_t mask1 = FStar_UInt32_eq_mask(a1, (uint32_t)0x3ffffffU);
-    uint32_t mask2 = FStar_UInt32_eq_mask(a2, (uint32_t)0x3ffffffU);
-    uint32_t mask3 = FStar_UInt32_eq_mask(a3, (uint32_t)0x3ffffffU);
-    uint32_t mask4 = FStar_UInt32_eq_mask(a4, (uint32_t)0x3ffffffU);
-    uint32_t mask = (((mask0 & mask1) & mask2) & mask3) & mask4;
-    uint32_t a0_ = a0 - ((uint32_t)0x3fffffbU & mask);
-    uint32_t a1_ = a1 - ((uint32_t)0x3ffffffU & mask);
-    uint32_t a2_ = a2 - ((uint32_t)0x3ffffffU & mask);
-    uint32_t a3_ = a3 - ((uint32_t)0x3ffffffU & mask);
-    uint32_t a4_ = a4 - ((uint32_t)0x3ffffffU & mask);
+    a0 = acc[0U];
+    a1 = acc[1U];
+    a2 = acc[2U];
+    a3 = acc[3U];
+    a4 = acc[4U];
+    mask0 = FStar_UInt32_gte_mask(a0, (uint32_t)0x3fffffbU);
+    mask1 = FStar_UInt32_eq_mask(a1, (uint32_t)0x3ffffffU);
+    mask2 = FStar_UInt32_eq_mask(a2, (uint32_t)0x3ffffffU);
+    mask3 = FStar_UInt32_eq_mask(a3, (uint32_t)0x3ffffffU);
+    mask4 = FStar_UInt32_eq_mask(a4, (uint32_t)0x3ffffffU);
+    mask = (((mask0 & mask1) & mask2) & mask3) & mask4;
+    a0_ = a0 - ((uint32_t)0x3fffffbU & mask);
+    a1_ = a1 - ((uint32_t)0x3ffffffU & mask);
+    a2_ = a2 - ((uint32_t)0x3ffffffU & mask);
+    a3_ = a3 - ((uint32_t)0x3ffffffU & mask);
+    a4_ = a4 - ((uint32_t)0x3ffffffU & mask);
     acc[0U] = a0_;
     acc[1U] = a1_;
     acc[2U] = a2_;
@@ -315,7 +383,10 @@
 static Hacl_Impl_Poly1305_32_State_poly1305_state
 Hacl_Impl_Poly1305_32_mk_state(uint32_t *r, uint32_t *h)
 {
-    return ((Hacl_Impl_Poly1305_32_State_poly1305_state){.r = r, .h = h });
+    Hacl_Impl_Poly1305_32_State_poly1305_state ret;
+    ret.r = r;
+    ret.h = h;
+    return (ret);
 }

 static void
@@ -327,8 +398,9 @@
     if (!(len1 == (uint64_t)0U)) {
         uint8_t *block = m;
         uint8_t *tail1 = m + (uint32_t)16U;
+        uint64_t len2;
         Hacl_Impl_Poly1305_32_poly1305_update(st, block);
-        uint64_t len2 = len1 - (uint64_t)1U;
+        len2 = len1 - (uint64_t)1U;
         Hacl_Standalone_Poly1305_32_poly1305_blocks(st, tail1, len2);
     }
 }
@@ -363,14 +435,17 @@
     uint32_t
         r4 =
             (uint32_t)FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t)104U)) & (uint32_t)0x3ffffffU;
+    Hacl_Impl_Poly1305_32_State_poly1305_state scrut0;
+    uint32_t *h;
+    uint32_t *x00;
     x0[0U] = r0;
     x0[1U] = r1;
     x0[2U] = r2;
     x0[3U] = r3;
     x0[4U] = r4;
-    Hacl_Impl_Poly1305_32_State_poly1305_state scrut0 = st;
-    uint32_t *h = scrut0.h;
-    uint32_t *x00 = h;
+    scrut0 = st;
+    h = scrut0.h;
+    x00 = h;
     x00[0U] = (uint32_t)0U;
     x00[1U] = (uint32_t)0U;
     x00[2U] = (uint32_t)0U;
@@ -391,12 +466,15 @@
     uint64_t rem16 = len1 & (uint64_t)0xfU;
     uint8_t *part_input = m;
     uint8_t *last_block = m + (uint32_t)((uint64_t)16U * len16);
+    Hacl_Impl_Poly1305_32_State_poly1305_state scrut;
+    uint32_t *h;
+    uint32_t *acc;
     Hacl_Standalone_Poly1305_32_poly1305_partial(st, part_input, len16, kr);
     if (!(rem16 == (uint64_t)0U))
         Hacl_Impl_Poly1305_32_poly1305_process_last_block(st, last_block, rem16);
-    Hacl_Impl_Poly1305_32_State_poly1305_state scrut = st;
-    uint32_t *h = scrut.h;
-    uint32_t *acc = h;
+    scrut = st;
+    h = scrut.h;
+    acc = h;
     Hacl_Impl_Poly1305_32_poly1305_last_pass(acc);
 }

@@ -410,20 +488,31 @@
     uint32_t buf[10U] = { 0U };
     uint32_t *r = buf;
     uint32_t *h = buf + (uint32_t)5U;
+    uint8_t *key_s;
+    Hacl_Impl_Poly1305_32_State_poly1305_state scrut;
+    uint32_t *h5;
+    uint32_t *acc;
+    FStar_UInt128_t k_;
+    uint32_t h0;
+    uint32_t h1;
+    uint32_t h2;
+    uint32_t h3;
+    uint32_t h4;
+    FStar_UInt128_t acc_;
+    FStar_UInt128_t mac_;
     Hacl_Impl_Poly1305_32_State_poly1305_state st = Hacl_Impl_Poly1305_32_mk_state(r, h);
-    uint8_t *key_s = k1 + (uint32_t)16U;
+    key_s = k1 + (uint32_t)16U;
     Hacl_Standalone_Poly1305_32_poly1305_complete(st, input, len1, k1);
-    Hacl_Impl_Poly1305_32_State_poly1305_state scrut = st;
-    uint32_t *h5 = scrut.h;
-    uint32_t *acc = h5;
-    FStar_UInt128_t k_ = load128_le(key_s);
-    uint32_t h0 = acc[0U];
-    uint32_t h1 = acc[1U];
-    uint32_t h2 = acc[2U];
-    uint32_t h3 = acc[3U];
-    uint32_t h4 = acc[4U];
-    FStar_UInt128_t
-        acc_ =
+    scrut = st;
+    h5 = scrut.h;
+    acc = h5;
+    k_ = load128_le(key_s);
+    h0 = acc[0U];
+    h1 = acc[1U];
+    h2 = acc[2U];
+    h3 = acc[3U];
+    h4 = acc[4U];
+    acc_ =
             FStar_UInt128_logor(FStar_UInt128_shift_left(FStar_UInt128_uint64_to_uint128((uint64_t)h4),
                                                          (uint32_t)104U),
                                 FStar_UInt128_logor(FStar_UInt128_shift_left(FStar_UInt128_uint64_to_uint128((uint64_t)h3),
@@ -433,7 +522,7 @@
                                                                         FStar_UInt128_logor(FStar_UInt128_shift_left(FStar_UInt128_uint64_to_uint128((uint64_t)h1),
                                                                                                                      (uint32_t)26U),
                                                                                             FStar_UInt128_uint64_to_uint128((uint64_t)h0)))));
-    FStar_UInt128_t mac_ = FStar_UInt128_add_mod(acc_, k_);
+    mac_ = FStar_UInt128_add_mod(acc_, k_);
     store128_le(output, mac_);
 }

@@ -485,14 +574,17 @@
     uint32_t
         r4 =
             (uint32_t)FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t)104U)) & (uint32_t)0x3ffffffU;
+    Hacl_Impl_Poly1305_32_State_poly1305_state scrut0;
+    uint32_t *h;
+    uint32_t *x00;
     x0[0U] = r0;
     x0[1U] = r1;
     x0[2U] = r2;
     x0[3U] = r3;
     x0[4U] = r4;
-    Hacl_Impl_Poly1305_32_State_poly1305_state scrut0 = st;
-    uint32_t *h = scrut0.h;
-    uint32_t *x00 = h;
+    scrut0 = st;
+    h = scrut0.h;
+    x00 = h;
     x00[0U] = (uint32_t)0U;
     x00[1U] = (uint32_t)0U;
     x00[2U] = (uint32_t)0U;
@@ -529,11 +621,14 @@
     uint8_t *m,
     uint32_t len1)
 {
+    Hacl_Impl_Poly1305_32_State_poly1305_state scrut;
+    uint32_t *h;
+    uint32_t *acc;
     if (!((uint64_t)len1 == (uint64_t)0U))
         Hacl_Impl_Poly1305_32_poly1305_process_last_block(st, m, (uint64_t)len1);
-    Hacl_Impl_Poly1305_32_State_poly1305_state scrut = st;
-    uint32_t *h = scrut.h;
-    uint32_t *acc = h;
+    scrut = st;
+    h = scrut.h;
+    acc = h;
     Hacl_Impl_Poly1305_32_poly1305_last_pass(acc);
 }

diff -ur misc/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.h misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.h
--- misc/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/Hacl_Poly1305_32.h	2018-10-22 00:11:45.152423000 -0700
@@ -13,6 +13,7 @@
  * limitations under the License.
  */

+#include "secport.h"
 #include "kremlib.h"
 #ifndef __Hacl_Poly1305_32_H
 #define __Hacl_Poly1305_32_H
diff -ur misc/nss-3.39/nss/lib/freebl/verified/kremlib_base.h misc/build/nss-3.39/nss/lib/freebl/verified/kremlib_base.h
--- misc/nss-3.39/nss/lib/freebl/verified/kremlib_base.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/freebl/verified/kremlib_base.h	2018-10-21 20:56:12.848112000 -0700
@@ -16,9 +16,26 @@
 #ifndef __KREMLIB_BASE_H
 #define __KREMLIB_BASE_H

-#include <inttypes.h>
+#if defined(_MSC_VER) && _MSC_VER < 1800
+ #define PRIx8	"x"
+ #define PRIx16	"x"
+ #define PRIx32	"x"
+ #ifdef _WIN64
+  #define PRIx64	"lx"
+ #else
+  #define PRIx64	"llx"
+ #endif
+#else
+ #include <inttypes.h>
+#endif
 #include <limits.h>
-#include <stdbool.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #define false 0
+ #define true 1
+typedef int bool;
+#else
+ #include <stdbool.h>
+#endif
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -47,6 +64,9 @@

 #ifdef __GNUC__
 #define inline __inline__
+#endif
+#if defined(_MSC_VER)
+#define inline __inline
 #endif

 /* GCC-specific attribute syntax; everyone else gets the standard C inline
diff -ur misc/nss-3.39/nss/lib/pk11wrap/pk11skey.c misc/build/nss-3.39/nss/lib/pk11wrap/pk11skey.c
--- misc/nss-3.39/nss/lib/pk11wrap/pk11skey.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/pk11wrap/pk11skey.c	2018-10-22 01:25:27.313788000 -0700
@@ -2217,12 +2217,13 @@
     /* old PKCS #11 spec was ambiguous on what needed to be passed,
      * try this again with an encoded public key */
     if (crv != CKR_OK) {
+        SECItem *pubValue;
         /* For curves that only use X as public value and no encoding we don't
          * have to try again. (Currently only Curve25519) */
         if (pk11_ECGetPubkeyEncoding(pubKey) == ECPoint_XOnly) {
             goto loser;
         }
-        SECItem *pubValue = SEC_ASN1EncodeItem(NULL, NULL,
+        pubValue = SEC_ASN1EncodeItem(NULL, NULL,
                                                &pubKey->u.ec.publicValue,
                                                SEC_ASN1_GET(SEC_OctetStringTemplate));
         if (pubValue == NULL) {
diff -ur misc/nss-3.39/nss/lib/pkcs7/p7create.c misc/build/nss-3.39/nss/lib/pkcs7/p7create.c
--- misc/nss-3.39/nss/lib/pkcs7/p7create.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/pkcs7/p7create.c	2018-10-22 10:00:01.127657000 -0700
@@ -1263,6 +1263,7 @@
     SECAlgorithmID *algid;
     SEC_PKCS7EncryptedData *enc_data;
     SECStatus rv;
+    SECAlgorithmID *pbe_algid;

     PORT_Assert(SEC_PKCS5IsAlgorithmPBEAlgTag(pbe_algorithm));

@@ -1274,7 +1275,6 @@
     enc_data = cinfo->content.encryptedData;
     algid = &(enc_data->encContentInfo.contentEncAlg);

-    SECAlgorithmID *pbe_algid;
     pbe_algid = PK11_CreatePBEV2AlgorithmID(pbe_algorithm,
                                             cipher_algorithm,
                                             prf_algorithm,
diff -ur misc/nss-3.39/nss/lib/softoken/pkcs11c.c misc/build/nss-3.39/nss/lib/softoken/pkcs11c.c
--- misc/nss-3.39/nss/lib/softoken/pkcs11c.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/softoken/pkcs11c.c	2018-10-22 01:08:34.274286000 -0700
@@ -5125,8 +5125,9 @@
                 crv = sftk_AddAttributeType(publicKey, CKA_EC_POINT,
                                             sftk_item_expand(&ecPriv->publicValue));
             } else {
+                SECItem *pubValue;
                 PORT_FreeArena(ecParams->arena, PR_TRUE);
-                SECItem *pubValue = SEC_ASN1EncodeItem(NULL, NULL,
+                pubValue = SEC_ASN1EncodeItem(NULL, NULL,
                                                        &ecPriv->publicValue,
                                                        SEC_ASN1_GET(SEC_OctetStringTemplate));
                 if (!pubValue) {
diff -ur misc/nss-3.39/nss/lib/softoken/sdb.c misc/build/nss-3.39/nss/lib/softoken/sdb.c
--- misc/nss-3.39/nss/lib/softoken/sdb.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/softoken/sdb.c	2018-10-22 01:18:14.220773000 -0700
@@ -206,12 +206,13 @@
 sdb_chmod(const char *filename, int pmode)
 {
     int result;
+    wchar_t *filenameWide;

     if (!filename) {
         return -1;
     }

-    wchar_t *filenameWide = _NSSUTIL_UTF8ToWide(filename);
+    filenameWide = _NSSUTIL_UTF8ToWide(filename);
     if (!filenameWide) {
         return -1;
     }
diff -ur misc/nss-3.39/nss/lib/ssl/dtls13con.c misc/build/nss-3.39/nss/lib/ssl/dtls13con.c
--- misc/nss-3.39/nss/lib/ssl/dtls13con.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/dtls13con.c	2018-10-22 01:31:19.795730000 -0700
@@ -64,7 +64,7 @@
 } DTLSHandshakeRecordEntry;

 /* Combine the epoch and sequence number into a single value. */
-static inline sslSequenceNumber
+static __inline sslSequenceNumber
 dtls_CombineSequenceNumber(DTLSEpoch epoch, sslSequenceNumber seqNum)
 {
     PORT_Assert(seqNum <= RECORD_SEQ_MAX);
diff -ur misc/nss-3.39/nss/lib/ssl/selfencrypt.c misc/build/nss-3.39/nss/lib/ssl/selfencrypt.c
--- misc/nss-3.39/nss/lib/ssl/selfencrypt.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/selfencrypt.c	2018-10-22 03:36:02.726686000 -0700
@@ -193,6 +193,14 @@
     PRUint8 *out, unsigned int *outLen, unsigned int maxOutLen)
 {
     sslReader reader = SSL_READER(in, inLen);
+    sslReadBuffer ivBuffer = { 0 };
+    PRUint64 cipherTextLen = 0;
+    sslReadBuffer cipherTextBuffer = { 0 };
+    unsigned int bytesToMac;
+    sslReadBuffer encodedMacBuffer = { 0 };
+    unsigned char computedMac[SHA256_LENGTH];
+    unsigned int computedMacLen = 0;
+    SECItem ivItem = { siBuffer, (unsigned char *)ivBuffer.buf, AES_BLOCK_SIZE };

     sslReadBuffer encodedKeyNameBuffer = { 0 };
     SECStatus rv = sslRead_Read(&reader, SELF_ENCRYPT_KEY_NAME_LEN,
@@ -201,26 +209,22 @@
         return SECFailure;
     }

-    sslReadBuffer ivBuffer = { 0 };
     rv = sslRead_Read(&reader, AES_BLOCK_SIZE, &ivBuffer);
     if (rv != SECSuccess) {
         return SECFailure;
     }

-    PRUint64 cipherTextLen = 0;
     rv = sslRead_ReadNumber(&reader, 2, &cipherTextLen);
     if (rv != SECSuccess) {
         return SECFailure;
     }

-    sslReadBuffer cipherTextBuffer = { 0 };
     rv = sslRead_Read(&reader, (unsigned int)cipherTextLen, &cipherTextBuffer);
     if (rv != SECSuccess) {
         return SECFailure;
     }
-    unsigned int bytesToMac = reader.offset;
+    bytesToMac = reader.offset;

-    sslReadBuffer encodedMacBuffer = { 0 };
     rv = sslRead_Read(&reader, SHA256_LENGTH, &encodedMacBuffer);
     if (rv != SECSuccess) {
         return SECFailure;
@@ -240,8 +244,6 @@
     }

     /* 2. Check the MAC */
-    unsigned char computedMac[SHA256_LENGTH];
-    unsigned int computedMacLen = 0;
     rv = ssl_MacBuffer(macKey, CKM_SHA256_HMAC, in, bytesToMac,
                        computedMac, &computedMacLen, sizeof(computedMac));
     if (rv != SECSuccess) {
@@ -254,7 +256,6 @@
     }

     /* 3. OK, it verifies, now decrypt. */
-    SECItem ivItem = { siBuffer, (unsigned char *)ivBuffer.buf, AES_BLOCK_SIZE };
     rv = PK11_Decrypt(encKey, CKM_AES_CBC_PAD, &ivItem,
                       out, outLen, maxOutLen, cipherTextBuffer.buf, cipherTextLen);
     if (rv != SECSuccess) {
diff -ur misc/nss-3.39/nss/lib/ssl/ssl3con.c misc/build/nss-3.39/nss/lib/ssl/ssl3con.c
--- misc/nss-3.39/nss/lib/ssl/ssl3con.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/ssl3con.c	2018-10-22 01:44:48.945390000 -0700
@@ -5718,6 +5718,7 @@
     SECStatus rv = SECFailure;
     SECItem enc_pms = { siBuffer, NULL, 0 };
     PRBool isTLS;
+    unsigned int svrPubKeyBits;

     PORT_Assert(ss->opt.noLocks || ssl_HaveSSL3HandshakeLock(ss));
     PORT_Assert(ss->opt.noLocks || ssl_HaveXmitBufLock(ss));
@@ -5734,7 +5735,7 @@
     }

     /* Get the wrapped (encrypted) pre-master secret, enc_pms */
-    unsigned int svrPubKeyBits = SECKEY_PublicKeyStrengthInBits(svrPubKey);
+    svrPubKeyBits = SECKEY_PublicKeyStrengthInBits(svrPubKey);
     enc_pms.len = (svrPubKeyBits + 7) / 8;
     /* Check that the RSA key isn't larger than 8k bit. */
     if (svrPubKeyBits > SSL_MAX_RSA_KEY_BITS) {
@@ -8123,6 +8124,7 @@
 ssl_GenerateServerRandom(sslSocket *ss)
 {
     SECStatus rv = ssl3_GetNewRandom(ss->ssl3.hs.server_random);
+    PRUint8 *downgradeSentinel;
     if (rv != SECSuccess) {
         return SECFailure;
     }
@@ -8154,7 +8156,7 @@
      *
      *   44 4F 57 4E 47 52 44 00
      */
-    PRUint8 *downgradeSentinel =
+    downgradeSentinel =
         ss->ssl3.hs.server_random +
         SSL3_RANDOM_LENGTH - sizeof(tls13_downgrade_random);

@@ -11986,11 +11988,13 @@
     }

     for (i = 0; i < toCheck; i++) {
+        unsigned char mask;
+        unsigned char b;
         t = paddingLength - i;
         /* If i <= paddingLength then the MSB of t is zero and mask is
          * 0xff.  Otherwise, mask is 0. */
-        unsigned char mask = DUPLICATE_MSB_TO_ALL(~t);
-        unsigned char b = plaintext->buf[plaintext->len - 1 - i];
+        mask = DUPLICATE_MSB_TO_ALL(~t);
+        b = plaintext->buf[plaintext->len - 1 - i];
         /* The final |paddingLength+1| bytes should all have the value
          * |paddingLength|. Therefore the XOR should be zero. */
         good &= ~(mask & (paddingLength ^ b));
@@ -12532,6 +12536,7 @@
     }

     if (rv != SECSuccess) {
+        int errCode;
         ssl_ReleaseSpecReadLock(ss); /***************************/

         SSL_DBG(("%d: SSL3[%d]: decryption failed", SSL_GETPID(), ss->fd));
@@ -12562,7 +12567,7 @@
             return SECSuccess;
         }

-        int errCode = PORT_GetError();
+        errCode = PORT_GetError();
         SSL3_SendAlert(ss, alert_fatal, alert);
         /* Reset the error code in case SSL3_SendAlert called
          * PORT_SetError(). */
diff -ur misc/nss-3.39/nss/lib/ssl/ssl3exthandle.c misc/build/nss-3.39/nss/lib/ssl/ssl3exthandle.c
--- misc/nss-3.39/nss/lib/ssl/ssl3exthandle.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/ssl3exthandle.c	2018-10-22 02:03:24.559698000 -0700
@@ -1915,6 +1915,8 @@
                            sslBuffer *buf, PRBool *added)
 {
     PRUint32 maxLimit;
+    PRUint32 limit;
+    SECStatus rv;
     if (ss->sec.isServer) {
         maxLimit = (ss->version >= SSL_LIBRARY_VERSION_TLS_1_3)
                        ? (MAX_FRAGMENT_LENGTH + 1)
@@ -1924,8 +1926,8 @@
                        ? (MAX_FRAGMENT_LENGTH + 1)
                        : MAX_FRAGMENT_LENGTH;
     }
-    PRUint32 limit = PR_MIN(ss->opt.recordSizeLimit, maxLimit);
-    SECStatus rv = sslBuffer_AppendNumber(buf, limit, 2);
+    limit = PR_MIN(ss->opt.recordSizeLimit, maxLimit);
+    rv = sslBuffer_AppendNumber(buf, limit, 2);
     if (rv != SECSuccess) {
         return SECFailure;
     }
diff -ur misc/nss-3.39/nss/lib/ssl/sslbloom.c misc/build/nss-3.39/nss/lib/ssl/sslbloom.c
--- misc/nss-3.39/nss/lib/ssl/sslbloom.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/sslbloom.c	2018-10-22 01:50:48.294197000 -0700
@@ -10,7 +10,7 @@
 #include "prnetdb.h"
 #include "secport.h"

-static inline unsigned int
+static __inline unsigned int
 sslBloom_Size(unsigned int bits)
 {
     return (bits >= 3) ? (1 << (bits - 3)) : 1;
diff -ur misc/nss-3.39/nss/lib/ssl/sslencode.c misc/build/nss-3.39/nss/lib/ssl/sslencode.c
--- misc/nss-3.39/nss/lib/ssl/sslencode.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/sslencode.c	2018-10-22 01:55:55.317356000 -0700
@@ -214,6 +214,8 @@
 SECStatus
 sslRead_ReadNumber(sslReader *reader, unsigned int bytes, PRUint64 *num)
 {
+    unsigned int i;
+    PRUint64 number = 0;
     if (!reader || !num) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
         return SECFailure;
@@ -224,8 +226,6 @@
         PORT_SetError(SEC_ERROR_BAD_DATA);
         return SECFailure;
     }
-    unsigned int i;
-    PRUint64 number = 0;
     for (i = 0; i < bytes; i++) {
         number = (number << 8) + reader->buf.buf[i + reader->offset];
     }
diff -ur misc/nss-3.39/nss/lib/ssl/sslnonce.c misc/build/nss-3.39/nss/lib/ssl/sslnonce.c
--- misc/nss-3.39/nss/lib/ssl/sslnonce.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/sslnonce.c	2018-10-22 02:55:25.098750000 -0700
@@ -439,6 +439,10 @@
 ssl_DecodeResumptionToken(sslSessionID *sid, const PRUint8 *encodedToken,
                           PRUint32 encodedTokenLen)
 {
+    sslReader reader;
+    PRUint64 tmpInt = 0;
+    sslReadBuffer readerBuffer = { 0 };
+
     PORT_Assert(encodedTokenLen);
     PORT_Assert(encodedToken);
     PORT_Assert(sid);
@@ -454,10 +458,11 @@
     }

     /* These variables are used across macros. Don't use them outside. */
-    sslReader reader = SSL_READER(encodedToken, encodedTokenLen);
+    // sslReader reader = SSL_READER(encodedToken, encodedTokenLen);
+    reader.buf.buf = encodedToken;
+    reader.buf.len = encodedTokenLen;
+    reader.offset = 0;
     reader.offset += 1; // We read the version already. Skip the first byte.
-    sslReadBuffer readerBuffer = { 0 };
-    PRUint64 tmpInt = 0;

     if (sslRead_ReadNumber(&reader, 8, &tmpInt) != SECSuccess) {
         return SECFailure;
@@ -494,9 +499,13 @@
         return SECFailure;
     }
     if (readerBuffer.len) {
+        SECItem tempItem;
         PORT_Assert(!sid->peerCert);
-        SECItem tempItem = { siBuffer, (unsigned char *)readerBuffer.buf,
-                             readerBuffer.len };
+        // tempItem = { siBuffer, (unsigned char *)readerBuffer.buf,
+        //                      readerBuffer.len };
+	tempItem.type = siBuffer;
+	tempItem.data = (unsigned char *)readerBuffer.buf;
+	tempItem.len = readerBuffer.len;
         sid->peerCert = CERT_NewTempCertificate(NULL, /* dbHandle */
                                                 &tempItem,
                                                 NULL, PR_FALSE, PR_TRUE);
@@ -510,12 +519,16 @@
         return SECFailure;
     }
     if (readerBuffer.len) {
+        SECItem tempItem;
         SECITEM_AllocArray(NULL, &sid->peerCertStatus, 1);
         if (!sid->peerCertStatus.items) {
             return SECFailure;
         }
-        SECItem tempItem = { siBuffer, (unsigned char *)readerBuffer.buf,
-                             readerBuffer.len };
+        // SECItem tempItem = { siBuffer, (unsigned char *)readerBuffer.buf,
+        //                      readerBuffer.len };
+	tempItem.type = siBuffer;
+	tempItem.data = (unsigned char *)readerBuffer.buf;
+	tempItem.len = readerBuffer.len;
         SECITEM_CopyItem(NULL, &sid->peerCertStatus.items[0], &tempItem);
     }

@@ -545,9 +558,13 @@
         return SECFailure;
     }
     if (readerBuffer.len) {
+        SECItem tempItem;
         PORT_Assert(!sid->localCert);
-        SECItem tempItem = { siBuffer, (unsigned char *)readerBuffer.buf,
-                             readerBuffer.len };
+        //SECItem tempItem = { siBuffer, (unsigned char *)readerBuffer.buf,
+        //                     readerBuffer.len };
+	tempItem.type = siBuffer;
+	tempItem.data = (unsigned char *)readerBuffer.buf;
+	tempItem.len = readerBuffer.len;
         sid->localCert = CERT_NewTempCertificate(NULL, /* dbHandle */
                                                  &tempItem,
                                                  NULL, PR_FALSE, PR_TRUE);
@@ -706,13 +723,15 @@
 PRBool
 ssl_IsResumptionTokenValid(sslSocket *ss)
 {
+    sslSessionID *sid;
+    PRTime endTime = 0;
+    NewSessionTicket *ticket;
     PORT_Assert(ss);
-    sslSessionID *sid = ss->sec.ci.sid;
+    sid = ss->sec.ci.sid;
     PORT_Assert(sid);

     // Check that the ticket didn't expire.
-    PRTime endTime = 0;
-    NewSessionTicket *ticket = &sid->u.ssl3.locked.sessionTicket;
+    ticket = &sid->u.ssl3.locked.sessionTicket;
     if (ticket->ticket_lifetime_hint != 0) {
         endTime = ticket->received_timestamp +
                   (PRTime)(ticket->ticket_lifetime_hint * PR_USEC_PER_SEC);
@@ -746,6 +765,9 @@
 static SECStatus
 ssl_EncodeResumptionToken(sslSessionID *sid, sslBuffer *encodedTokenBuf)
 {
+    SECStatus rv;
+    PRUint64 len;
+
     PORT_Assert(encodedTokenBuf);
     PORT_Assert(sid);
     if (!sid || !sid->u.ssl3.locked.sessionTicket.ticket.len ||
@@ -760,7 +782,7 @@
      * SECItems are prepended with a 64-bit length field followed by the bytes.
      * Optional bytes are encoded as a 0-length item if not present.
      */
-    SECStatus rv = sslBuffer_AppendNumber(encodedTokenBuf,
+    rv = sslBuffer_AppendNumber(encodedTokenBuf,
                                           SSLResumptionTokenVersion, 1);
     if (rv != SECSuccess) {
         return SECFailure;
@@ -843,7 +865,7 @@
         }
     }

-    PRUint64 len = sid->peerID ? strlen(sid->peerID) : 0;
+    len = sid->peerID ? strlen(sid->peerID) : 0;
     if (len > PR_UINT8_MAX) {
         // This string really shouldn't be that long.
         PORT_SetError(SEC_ERROR_LIBRARY_FAILURE);
@@ -1052,8 +1074,11 @@
 void
 ssl_CacheExternalToken(sslSocket *ss)
 {
+    sslSessionID *sid;
+    sslBuffer encodedToken = SSL_BUFFER_EMPTY;
+
     PORT_Assert(ss);
-    sslSessionID *sid = ss->sec.ci.sid;
+    sid = ss->sec.ci.sid;
     PORT_Assert(sid);
     PORT_Assert(sid->cached == never_cached);
     PORT_Assert(ss->resumptionTokenCallback);
@@ -1083,8 +1108,6 @@
         sid->expirationTime = sid->creationTime + ssl3_sid_timeout;
     }

-    sslBuffer encodedToken = SSL_BUFFER_EMPTY;
-
     if (ssl_EncodeResumptionToken(sid, &encodedToken) != SECSuccess) {
         SSL_TRC(3, ("SSL [%d]: encoding resumption token failed", ss->fd));
         return;
@@ -1127,11 +1150,12 @@
 void
 ssl_UncacheSessionID(sslSocket *ss)
 {
+    sslSecurityInfo *sec;
     if (ss->opt.noCache) {
         return;
     }

-    sslSecurityInfo *sec = &ss->sec;
+    sec = &ss->sec;
     PORT_Assert(sec);

     if (sec->ci.sid) {
diff -ur misc/nss-3.39/nss/lib/ssl/sslsnce.c misc/build/nss-3.39/nss/lib/ssl/sslsnce.c
--- misc/nss-3.39/nss/lib/ssl/sslsnce.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/sslsnce.c	2018-10-22 03:10:53.707928000 -0700
@@ -732,11 +732,11 @@
 void
 ssl_ServerCacheSessionID(sslSessionID *sid)
 {
-    PORT_Assert(sid);
-
     sidCacheEntry sce;
     PRUint32 now = 0;
     cacheDesc *cache = &globalCache;
+
+    PORT_Assert(sid);

     if (sid->u.ssl3.sessionIDLength == 0) {
         return;
diff -ur misc/nss-3.39/nss/lib/ssl/sslsock.c misc/build/nss-3.39/nss/lib/ssl/sslsock.c
--- misc/nss-3.39/nss/lib/ssl/sslsock.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/sslsock.c	2018-10-22 03:26:21.638950000 -0700
@@ -53,38 +53,38 @@
 ** default settings for socket enables
 */
 static sslOptions ssl_defaults = {
-    .nextProtoNego = { siBuffer, NULL, 0 },
-    .maxEarlyDataSize = 1 << 16,
-    .recordSizeLimit = MAX_FRAGMENT_LENGTH + 1,
-    .useSecurity = PR_TRUE,
-    .useSocks = PR_FALSE,
-    .requestCertificate = PR_FALSE,
-    .requireCertificate = SSL_REQUIRE_FIRST_HANDSHAKE,
-    .handshakeAsClient = PR_FALSE,
-    .handshakeAsServer = PR_FALSE,
-    .noCache = PR_FALSE,
-    .fdx = PR_FALSE,
-    .detectRollBack = PR_TRUE,
-    .noLocks = PR_FALSE,
-    .enableSessionTickets = PR_FALSE,
-    .enableDeflate = PR_FALSE,
-    .enableRenegotiation = SSL_RENEGOTIATE_REQUIRES_XTN,
-    .requireSafeNegotiation = PR_FALSE,
-    .enableFalseStart = PR_FALSE,
-    .cbcRandomIV = PR_TRUE,
-    .enableOCSPStapling = PR_FALSE,
-    .enableALPN = PR_TRUE,
-    .reuseServerECDHEKey = PR_TRUE,
-    .enableFallbackSCSV = PR_FALSE,
-    .enableServerDhe = PR_TRUE,
-    .enableExtendedMS = PR_FALSE,
-    .enableSignedCertTimestamps = PR_FALSE,
-    .requireDHENamedGroups = PR_FALSE,
-    .enable0RttData = PR_FALSE,
-    .enableTls13CompatMode = PR_FALSE,
-    .enableDtlsShortHeader = PR_FALSE,
-    .enableHelloDowngradeCheck = PR_FALSE,
-    .enableV2CompatibleHello = PR_FALSE
+    /* .nextProtoNego = */ { siBuffer, NULL, 0 },
+    /* .recordSizeLimit = */ MAX_FRAGMENT_LENGTH + 1,
+    /* .maxEarlyDataSize = */ 1 << 16,
+    /* .useSecurity = */ PR_TRUE,
+    /* .useSocks = */ PR_FALSE,
+    /* .requestCertificate = */ PR_FALSE,
+    /* .requireCertificate = */ SSL_REQUIRE_FIRST_HANDSHAKE,
+    /* .handshakeAsClient = */ PR_FALSE,
+    /* .handshakeAsServer = */ PR_FALSE,
+    /* .noCache = */ PR_FALSE,
+    /* .fdx = */ PR_FALSE,
+    /* .detectRollBack = */ PR_TRUE,
+    /* .noLocks = */ PR_FALSE,
+    /* .enableSessionTickets = */ PR_FALSE,
+    /* .enableDeflate = */ PR_FALSE,
+    /* .enableRenegotiation = */ SSL_RENEGOTIATE_REQUIRES_XTN,
+    /* .requireSafeNegotiation = */ PR_FALSE,
+    /* .enableFalseStart = */ PR_FALSE,
+    /* .cbcRandomIV = */ PR_TRUE,
+    /* .enableOCSPStapling = */ PR_FALSE,
+    /* .enableALPN = */ PR_TRUE,
+    /* .reuseServerECDHEKey = */ PR_TRUE,
+    /* .enableFallbackSCSV = */ PR_FALSE,
+    /* .enableServerDhe = */ PR_TRUE,
+    /* .enableExtendedMS = */ PR_FALSE,
+    /* .enableSignedCertTimestamps = */ PR_FALSE,
+    /* .requireDHENamedGroups = */ PR_FALSE,
+    /* .enable0RttData = */ PR_FALSE,
+    /* .enableTls13CompatMode = */ PR_FALSE,
+    /* .enableDtlsShortHeader = */ PR_FALSE,
+    /* .enableHelloDowngradeCheck = */ PR_FALSE,
+    /* .enableV2CompatibleHello = */ PR_FALSE
 };

 /*
@@ -2032,6 +2032,7 @@
                      unsigned int length)
 {
     sslSocket *ss;
+    size_t firstLen;

     ss = ssl_FindSocket(fd);
     if (!ss) {
@@ -2050,7 +2051,7 @@
     ssl_GetSSL3HandshakeLock(ss);
     SECITEM_FreeItem(&ss->opt.nextProtoNego, PR_FALSE);
     SECITEM_AllocItem(NULL, &ss->opt.nextProtoNego, length);
-    size_t firstLen = data[0] + 1;
+    firstLen = data[0] + 1;
     /* firstLen <= length is ensured by ssl3_ValidateAppProtocol. */
     PORT_Memcpy(ss->opt.nextProtoNego.data + (length - firstLen), data, firstLen);
     PORT_Memcpy(ss->opt.nextProtoNego.data, data + firstLen, length - firstLen);
@@ -4079,6 +4080,7 @@
                           unsigned int len)
 {
     sslSocket *ss = ssl_FindSocket(fd);
+    SECStatus rv;

     if (!ss) {
         SSL_DBG(("%d: SSL[%d]: bad socket in SSL_SetResumptionToken",
@@ -4109,7 +4111,7 @@
     }

     /* Populate NewSessionTicket values */
-    SECStatus rv = ssl_DecodeResumptionToken(ss->sec.ci.sid, token, len);
+    rv = ssl_DecodeResumptionToken(ss->sec.ci.sid, token, len);
     if (rv != SECSuccess) {
         // If decoding fails, we assume the token is bad.
         PORT_SetError(SSL_ERROR_BAD_RESUMPTION_TOKEN_ERROR);
@@ -4163,13 +4165,14 @@
 SSLExp_GetResumptionTokenInfo(const PRUint8 *tokenData, unsigned int tokenLen,
                               SSLResumptionTokenInfo *tokenOut, PRUintn len)
 {
+    sslSessionID sid = { 0 };
+    SSLResumptionTokenInfo token;
+
     if (!tokenData || !tokenOut || !tokenLen ||
         len > sizeof(SSLResumptionTokenInfo)) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
         return SECFailure;
     }
-    sslSessionID sid = { 0 };
-    SSLResumptionTokenInfo token;

     /* Populate sid values */
     if (ssl_DecodeResumptionToken(&sid, tokenData, tokenLen) != SECSuccess) {
diff -ur misc/nss-3.39/nss/lib/ssl/tls13exthandle.c misc/build/nss-3.39/nss/lib/ssl/tls13exthandle.c
--- misc/nss-3.39/nss/lib/ssl/tls13exthandle.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/tls13exthandle.c	2018-10-22 03:41:59.569200000 -0700
@@ -773,6 +773,7 @@
                                      sslBuffer *buf, PRBool *added)
 {
     SECStatus rv;
+    PRUint16 ver;

     if (ss->version < SSL_LIBRARY_VERSION_TLS_1_3) {
         return SECSuccess;
@@ -781,7 +782,7 @@
     SSL_TRC(3, ("%d: TLS13[%d]: server send supported_versions extension",
                 SSL_GETPID(), ss->fd));

-    PRUint16 ver = tls13_EncodeDraftVersion(SSL_LIBRARY_VERSION_TLS_1_3,
+    ver = tls13_EncodeDraftVersion(SSL_LIBRARY_VERSION_TLS_1_3,
                                             ss->protocolVariant);
     rv = sslBuffer_AppendNumber(buf, ver, 2);
     if (rv != SECSuccess) {
diff -ur misc/nss-3.39/nss/lib/ssl/tls13hashstate.c misc/build/nss-3.39/nss/lib/ssl/tls13hashstate.c
--- misc/nss-3.39/nss/lib/ssl/tls13hashstate.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/ssl/tls13hashstate.c	2018-10-22 04:03:39.133885000 -0700
@@ -95,6 +95,9 @@
     PRUint64 group;
     const sslNamedGroupDef *selectedGroup;
     PRUint64 appTokenLen;
+    sslReader reader = SSL_READER(plaintext, plaintextLen);
+    sslReadBuffer appTokenReader = { 0 };
+    unsigned int hashLen;

     rv = ssl_SelfEncryptUnprotect(ss, cookie, cookieLen,
                                   plaintext, &plaintextLen, sizeof(plaintext));
@@ -102,7 +105,10 @@
         return SECFailure;
     }

-    sslReader reader = SSL_READER(plaintext, plaintextLen);
+    // reader = SSL_READER(plaintext, plaintextLen);
+    reader.buf.buf = plaintext;
+    reader.buf.len = plaintextLen;
+    reader.offset = 0;

     /* Should start with 0xff. */
     rv = sslRead_ReadNumber(&reader, 1, &sentinel);
@@ -138,7 +144,6 @@
         return SECFailure;
     }
     ss->xtnData.applicationToken.len = appTokenLen;
-    sslReadBuffer appTokenReader = { 0 };
     rv = sslRead_Read(&reader, appTokenLen, &appTokenReader);
     if (rv != SECSuccess) {
         FATAL_ERROR(ss, SSL_ERROR_RX_MALFORMED_CLIENT_HELLO, illegal_parameter);
@@ -148,7 +153,7 @@
     PORT_Memcpy(ss->xtnData.applicationToken.data, appTokenReader.buf, appTokenLen);

     /* The remainder is the hash. */
-    unsigned int hashLen = SSL_READER_REMAINING(&reader);
+    hashLen = SSL_READER_REMAINING(&reader);
     if (hashLen != tls13_GetHashSize(ss)) {
         FATAL_ERROR(ss, SSL_ERROR_RX_MALFORMED_CLIENT_HELLO, illegal_parameter);
         return SECFailure;
diff -ur misc/nss-3.39/nss/lib/util/quickder.c misc/build/nss-3.39/nss/lib/util/quickder.c
--- misc/nss-3.39/nss/lib/util/quickder.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/util/quickder.c	2018-09-10 17:24:47.548844000 -0700
@@ -408,11 +408,12 @@
 {
     const SEC_ASN1Template* ptrTemplate =
         SEC_ASN1GetSubtemplate(templateEntry, dest, PR_FALSE);
+    void* subdata;
     if (!ptrTemplate) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
         return SECFailure;
     }
-    void* subdata = PORT_ArenaZAlloc(arena, ptrTemplate->size);
+    subdata = PORT_ArenaZAlloc(arena, ptrTemplate->size);
     *(void**)((char*)dest + templateEntry->offset) = subdata;
     if (subdata) {
         return DecodeItem(subdata, ptrTemplate, src, arena, checkTag);
diff -ur misc/nss-3.39/nss/lib/util/secport.c misc/build/nss-3.39/nss/lib/util/secport.c
--- misc/nss-3.39/nss/lib/util/secport.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/util/secport.c	2018-10-21 01:46:42.919736000 -0700
@@ -21,7 +21,23 @@
 #include "prenv.h"
 #include "prinit.h"

-#include <stdint.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #ifdef _WIN64
+typedef unsigned __int64 uintptr_t;
+ #else
+typedef unsigned int uintptr_t;
+ #endif
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned __int64 uint64_t;
+#define UINT8_MAX	0xff
+#define UINT16_MAX	0xffff
+#define UINT32_MAX	0xffffffffu
+#define UINT64_MAX	0xffffffffffffffffU
+#else
+ #include <stdint.h>
+#endif

 #ifdef DEBUG
 #define THREADMARK
@@ -150,13 +166,14 @@
 void *
 PORT_ZAllocAlignedOffset(size_t size, size_t alignment, size_t offset)
 {
+    void *mem = NULL;
+    void *v;
     PORT_Assert(offset < size);
     if (offset > size) {
         return NULL;
     }

-    void *mem = NULL;
-    void *v = PORT_ZAllocAligned(size, alignment, &mem);
+    v = PORT_ZAllocAligned(size, alignment, &mem);
     if (!v) {
         return NULL;
     }
diff -ur misc/nss-3.39/nss/lib/util/secport.h misc/build/nss-3.39/nss/lib/util/secport.h
--- misc/nss-3.39/nss/lib/util/secport.h	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/util/secport.h	2018-10-21 20:43:01.473838000 -0700
@@ -45,7 +45,30 @@
 #include <string.h>
 #include <stddef.h>
 #include <stdlib.h>
-#include <stdint.h>
+#if defined(_MSC_VER) && _MSC_VER < 1600
+ #ifdef _WIN64
+typedef unsigned __int64 uintptr_t;
+ #else
+typedef unsigned int uintptr_t;
+ #endif
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned __int64 uint64_t;
+typedef char int8_t;
+typedef short int16_t;
+typedef int int32_t;
+typedef __int64 int64_t;
+#define UINT8_MAX      0xff
+#define UINT16_MAX     0xffff
+#define UINT32_MAX     0xffffffffu
+#define UINT64_MAX     0xffffffffffffffffU
+#define UINT64_C(x)    ((x) + (UINT64_MAX - UINT64_MAX))
+#define INT32_MIN     (-0x7fffffff - 1)
+#define INT32_MAX     0x7fffffff
+#else
+ #include <stdint.h>
+#endif
 #include "prtypes.h"
 #include "prlog.h" /* for PR_ASSERT */
 #include "plarena.h"
diff -ur misc/nss-3.39/nss/lib/util/utilmod.c misc/build/nss-3.39/nss/lib/util/utilmod.c
--- misc/nss-3.39/nss/lib/util/utilmod.c	2018-08-31 05:55:53.000000000 -0700
+++ misc/build/nss-3.39/nss/lib/util/utilmod.c	2018-09-11 01:58:56.505884000 -0700
@@ -75,12 +75,13 @@
 os_open(const char *filename, int oflag, int pmode)
 {
     int fd;
+    wchar_t *filenameWide;

     if (!filename) {
         return -1;
     }

-    wchar_t *filenameWide = _NSSUTIL_UTF8ToWide(filename);
+    filenameWide = _NSSUTIL_UTF8ToWide(filename);
     if (!filenameWide) {
         return -1;
     }
@@ -94,12 +95,13 @@
 os_stat(const char *path, os_stat_type *buffer)
 {
     int result;
+    wchar_t *pathWide;

     if (!path) {
         return -1;
     }

-    wchar_t *pathWide = _NSSUTIL_UTF8ToWide(path);
+    pathWide = _NSSUTIL_UTF8ToWide(path);
     if (!pathWide) {
         return -1;
     }
@@ -113,16 +115,18 @@
 os_fopen(const char *filename, const char *mode)
 {
     FILE *fp;
+    wchar_t *filenameWide;
+    wchar_t *modeWide;

     if (!filename || !mode) {
         return NULL;
     }

-    wchar_t *filenameWide = _NSSUTIL_UTF8ToWide(filename);
+    filenameWide = _NSSUTIL_UTF8ToWide(filename);
     if (!filenameWide) {
         return NULL;
     }
-    wchar_t *modeWide = _NSSUTIL_UTF8ToWide(mode);
+    modeWide = _NSSUTIL_UTF8ToWide(mode);
     if (!modeWide) {
         PORT_Free(filenameWide);
         return NULL;
@@ -138,12 +142,13 @@
 _NSSUTIL_Access(const char *path, PRAccessHow how)
 {
     int result;
+    int mode;
+    wchar_t *pathWide;

     if (!path) {
         return PR_FAILURE;
     }

-    int mode;
     switch (how) {
         case PR_ACCESS_WRITE_OK:
             mode = 2;
@@ -158,7 +163,7 @@
             return PR_FAILURE;
     }

-    wchar_t *pathWide = _NSSUTIL_UTF8ToWide(path);
+    pathWide = _NSSUTIL_UTF8ToWide(path);
     if (!pathWide) {
         return PR_FAILURE;
     }
@@ -172,12 +177,13 @@
 nssutil_Delete(const char *name)
 {
     BOOL result;
+    wchar_t *nameWide;

     if (!name) {
         return PR_FAILURE;
     }

-    wchar_t *nameWide = _NSSUTIL_UTF8ToWide(name);
+    nameWide = _NSSUTIL_UTF8ToWide(name);
     if (!nameWide) {
         return PR_FAILURE;
     }
@@ -191,16 +197,18 @@
 nssutil_Rename(const char *from, const char *to)
 {
     BOOL result;
+    wchar_t *fromWide;
+    wchar_t *toWide;

     if (!from || !to) {
         return PR_FAILURE;
     }

-    wchar_t *fromWide = _NSSUTIL_UTF8ToWide(from);
+    fromWide = _NSSUTIL_UTF8ToWide(from);
     if (!fromWide) {
         return PR_FAILURE;
     }
-    wchar_t *toWide = _NSSUTIL_UTF8ToWide(to);
+    toWide = _NSSUTIL_UTF8ToWide(to);
     if (!toWide) {
         PORT_Free(fromWide);
         return PR_FAILURE;