EverParse/3d v2020.02.25

Changes from v2020.02.20:

• 3d: support for "external" macros (thanks @nikswamy ). Currently, such external macros must be defined as part of the 3d "prelude" library.
• 3d-generated files now use Windows' BOOLEAN type. This type is redefined in EverParseEndianness.h for non-Windows platforms.
• EverParseError.h no longer needed. Error handling now becomes per-module (thanks @nikswamy )

EverParse/3d v2020.02.20

Changes from v2020.02.14:

• 3d: support for several variable-length fields at the end of a struct (thanks @nikswamy )
• 3d: new syntax t field[<= length] for one-element fields of bounded variable length (thanks @nikswamy )
• QuackyDucky is now working. (However, in the Windows binary package, QuackyDucky support is still not included in everparse.bat, although bin\qd.exe will work.)
• Restored tests

EverParse/3d v2020.02.14

This release is for the 3d (not QuackyDucky) mode of EverParse.

Binaries

At this point we provide binary packages for Windows and MSVC only.

The binary package is self-contained: it contains EverParse/3d and all its dependencies (F*, kremlin, Z3.)

No external dependencies are needed (in particular, neither Cygwin nor OCaml.)

Sources

To use the source package:

0. You need the dependencies of Project Everest.
   In particular, for Windows, you need Cygwin, git and OCaml. Once you install Cygwin and git, you can automatically download and install other Project Everest dependencies by cloning Everest and running ./everest check
   On other platforms (e.g. Linux), ./everest check will check for your dependencies, but it will not install them.
1. Download the F* sources for branch nik_rename_let, and set the FSTAR_HOME environment variable to point to them
2. Download the KReMLin sources for branch master, and set the KREMLIN_HOME environment variable to point to them
3. To build EverParse/3d, do make 3d
4. To verify, build and run tests based on 3d, do make 3d-test.
5. (Windows only) To build the binary package, do make package