Barry Bond

This is non-blocking. I have a workaround. In F* code, if I write U64.(0UL -^ 1UL), I expect the result to be 64-bit 0xff...ffUL. But in the extracted C code,...

Remove explicit casts from some integer constants, to improve readability

2

Kremlin is careful to produce constant values with predictable behavior, despite ambiguities in C about integer promotion due to sizeof(int) and signed-ness of char. Examples: - (uint32_t)1U - (uint32_t)0U -...

Add support for building from VS2017

12

I tried installing just VS2017. It has the ability to install the VS2015 toolchain, so although the IDE is newer, the tools don't have to be. On a fresh Windows...

On Windows/cygwin, check if file "%WindowsSdkDir%include\%WindowsSdkVersion%\ucrt\inttypes.h" exists, and suggest installing a Windows 10 SDK if not. Those env vars are set by the Visual Studio Command Prompt script. If they...

EXT vs ML effect mismatch in Platform.Tcp.recv

3

See .fstar/ucontrib/Platform/fst/Platform.Tcp.fst: "assume val recv: networkStream -> max:nat -> EXT (optResult string (b:bytes {length b

In the diff view, I'd like to be able to select a C++ type or function and right-click to get to "go to definition" or "go to reference".