Articles

  • No categories

Wyjc

This page provides information on the Whiley-to-JVM (wyjc) compiler. It assumes you have already downloaded and installed the Whiley Development Kit (if not, see the getting started page).

Introduction

The Whiley-to-JVM Compiler (wyjc) is a command-line tool for compiling Whiley programs down to the Java Virtual Machine (JVM).  Currently, this is the only way to compile Whiley programs.  Wyjc is distributed as part of the Whiley Development Kit and uses wyjvm (for writing JVM classfiles) and wyone (for performing compile time checking of constraints).

Overview

Command-Line Options

The Whiley-to-Java Compiler (wyjc) has a number of command-line options:

Command Description
-whileypath <path> Set the CLASSPATH where wjc looks for (compiled) Whiley classes.
-bootpath <path> Set the CLASSPATH where wjc looks for (compiled) Whiley standard library classes.
-nvc Disable verification checking. This means the compiler will not perform any extended static checking and, hence, potential errors may exist in the compiled code. This option is particularly useful when debugging.
-nrc Disable runtime checking. This means the compiler will not insert any runtime checks into the code and, hence, errors will not be identified immediately when they arise. This option is particularly useful when debugging, and it also offers improved performance in cases where there are a large number of runtime checks.
-debug:lexer Print debug information from lexer.
-debug:checks Write debug information about generated runtime checks into a file with extension “.debug”.
-debug:pcs Write debug information about generated intermediate post-conditions into a file with extension “.debug”.
-debug:vcs Write debug information about generated verification conditions into a file with extension “.debug”.

Further Reading