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”. |
Popular Posts