Skip to content

INSTALL.md

Latest commit

 

History

History
69 lines (42 loc) · 2.58 KB

INSTALL.md

File metadata and controls

69 lines (42 loc) · 2.58 KB

Compiling WhyR From Source

To compile WhyR, you will need the following programs installed:

  • GNU Make or compatible make software, any recent version
  • Flex and Bison, any recent version
  • GNU G++, at least version 5
  • LLVM with development packages, version 3.7.1 exactly

Ensure that the correct version of g++ and LLVM is available in the default location the compiler will expect. If that's not possible, see 'Compilation Options' below.

Once this repository is cloned, navigate to this project's director and run:

make

This should build a WhyR debug build from sources. Look for the executable under the folder Debug.

Compilation Options

To alter the C++ compiler used, one can alter the Make variable CXX like so:

make GXX=(your c++ location)

Altering the LLVM lookup path is harder, because it is required for its includes, libraries, and binaries. Try modifying the Make variable CXXFLAGS to suit your needs.

There are more options not listed here. Look at the Makefile for a list of all of them.

Building a Release

To build a non-debug version of WhyR, run the following:

make build_release

The generated executable will be found in the Release folder.

Known Working Compilation Targets

  • Linux
  • Found to be working on Ubuntu and derivatives.
  • Windows
  • Requires Cygwin to properly compile.

Running WhyR

Running WhyR, whether from binary or from source, requires LLVM to be installed, version 3.7.1 exactly. Get LLVM from here if you don't have it.

whyr takes one positional argument- the LLVM bitcode (.bc) file to parse. There are flags for controlling output; run whyr without any arguments to see all of them. Errors and warnings will be printed to standard error. By default, WhyR prints the Why3 file generated to standard output.

Companion Programs

You will need Why3 installed on your machine in order to prove the files generated by WhyR. Get Why3 here.

In addition, Why3 requires at least one SMT solver application in order to prove programs. The Why3 website has an exhaustive list; suggested provers include Alt-Ergo, Z3, or CVC4.

WhyR Unit Tests

WhyR uses Google Test to run unit tests. No installation of Google Test is necessary; WhyR installs it for you. Compiling and running WhyR's test suite is as simple as running:

make test

It will run tests, and give an indication if any have failed.