wyc.commands

Class Compile

java.lang.Object

wyc.util.AbstractProjectCommand<Compile.Result>

wyc.commands.Compile

All Implemented Interfaces:

wycc.lang.Command<Compile.Result>, wycc.lang.Feature, wycc.lang.Feature.Configurable

public class Compile
extends AbstractProjectCommand<Compile.Result>

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Compile.Result Result kind for this command

Nested classes/interfaces inherited from interface wycc.lang.Feature

wycc.lang.Feature.Configurable, wycc.lang.Feature.ConfigurationError

Field Summary

Fields

Modifier and Type	Field and Description
protected boolean	brief Signals that brief error reporting should be used.
protected boolean	counterexamples Signals that counterexample generation should be performed.
protected boolean	proof Signals the proof should be printed during verification.
protected boolean	verbose Signals that verbose output should be produced.
protected boolean	verificationConditions Signals that verification conditions should be generated even if verification is not performed.
protected boolean	verify Signals that compile-time verification of source files should be performed.
protected wyfs.lang.Content.Filter<WhileyFile>	whileyExcludes Identifies which whiley sources files should not be considered for compilation.
protected wyfs.lang.Content.Filter<WhileyFile>	whileyIncludes Identifies which whiley source files should be considered for compilation.
protected wyfs.lang.Content.Filter<WyilFile>	wyilExcludes Identifies which wyil sources files should not be considered for compilation.
protected wyfs.lang.Content.Filter<WyilFile>	wyilIncludes Identifies which wyil source files should be considered for compilation.

Fields inherited from class wyc.util.AbstractProjectCommand

logger, registry, whileydir, whileypath, wyaldir, wycsdir, wyildir

Constructor Summary

Constructors

Constructor and Description
Compile(wyfs.lang.Content.Registry registry, wycc.util.Logger logger) Construct a new instance of this command.
Compile(wyfs.lang.Content.Registry registry, wycc.util.Logger logger, OutputStream sysout, OutputStream syserr) Construct a new instance of this command.

Method Summary

Modifier and Type	Method and Description
protected void	addCompilationBuildRules(wybs.util.StdProject project) Add build rules necessary for compiling whiley source files into binary wyil files.
protected void	addVerificationBuildRules(wybs.util.StdProject project) Add build rules necessary for compiling wyil binary files into wyal files for verification.
protected void	addWhiley2WyilBuildRule(wybs.util.StdProject project) Add the rule for compiling Whiley source files into WyIL files.
protected Compile.Result	compile(wybs.util.StdProject project, List<? extends wyfs.lang.Path.Entry<?>> entries)
String	describe(String option)
String	describeExcludes()
String	describeIncludes()
Compile.Result	execute(List<? extends wyfs.lang.Path.Entry<?>> entries)
Compile.Result	execute(String... args)
void	findCounterexamples(wyal.lang.WyalFile.Declaration.Assert assertion, wybs.util.StdProject project)
String	getDescription()
List	getModifiedSourceFiles()
static <T,S> List<wyfs.lang.Path.Entry<T>>	getModifiedSourceFiles(wyfs.lang.Path.Root sourceDir, wyfs.lang.Content.Filter<T> sourceIncludes, wyfs.lang.Path.Root binaryDir, wyfs.lang.Content.Type<S> binaryContentType) Generate the list of source files which need to be recompiled.
String	getName()
String[]	getOptions()
boolean	getVerificationConditions()
boolean	getVerify()
void	set(String option, Object value)
void	setBrief()
void	setExcludes(wyfs.lang.Content.Filter<WhileyFile> excludes)
void	setIncludes(wyfs.lang.Content.Filter<WhileyFile> includes)
void	setVerbose()
void	setVerbose(boolean b)
void	setVerificationConditions(boolean flag)
void	setVerify(boolean flag)

Methods inherited from class wyc.util.AbstractProjectCommand

addBootpath, finaliseConfiguration, get, getAbstractRoot, getDirectoryRoot, initialiseProject, setWhileydir, setWhileypath, setWyaldir, setWyildir

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

verbose

protected boolean verbose

Signals that verbose output should be produced.

brief

protected boolean brief

Signals that brief error reporting should be used. This is primarily used to help integration with external tools. More specifically, brief output is structured so as to be machine readable.

verify

protected boolean verify

Signals that compile-time verification of source files should be performed.

counterexamples

protected boolean counterexamples

Signals that counterexample generation should be performed.

verificationConditions

protected boolean verificationConditions

Signals that verification conditions should be generated even if verification is not performed.

proof

protected boolean proof

Signals the proof should be printed during verification.

whileyIncludes

protected wyfs.lang.Content.Filter<WhileyFile> whileyIncludes

Identifies which whiley source files should be considered for compilation. By default, all files reachable from srcdir are considered.

whileyExcludes

protected wyfs.lang.Content.Filter<WhileyFile> whileyExcludes

Identifies which whiley sources files should not be considered for compilation. This overrides any identified by whileyIncludes . By default, no files files reachable from srcdir are excluded.

wyilIncludes

protected wyfs.lang.Content.Filter<WyilFile> wyilIncludes

Identifies which wyil source files should be considered for compilation. By default, all files reachable from srcdir are considered.

wyilExcludes

protected wyfs.lang.Content.Filter<WyilFile> wyilExcludes

Identifies which wyil sources files should not be considered for compilation. This overrides any identified by whileyIncludes . By default, no files files reachable from srcdir are excluded.

Constructor Detail

Compile

public Compile(wyfs.lang.Content.Registry registry,
               wycc.util.Logger logger)

Construct a new instance of this command.

Parameters:

registry - The content registry being used to match files to content types.

Throws:

IOException

Compile

public Compile(wyfs.lang.Content.Registry registry,
               wycc.util.Logger logger,
               OutputStream sysout,
               OutputStream syserr)

Construct a new instance of this command.

Parameters:

registry - The content registry being used to match files to content types.

Throws:

IOException

Method Detail

getName

public String getName()

getOptions

public String[] getOptions()

Specified by:

getOptions in interface wycc.lang.Feature.Configurable

Overrides:

getOptions in class AbstractProjectCommand<Compile.Result>

describe

public String describe(String option)

Specified by:

describe in interface wycc.lang.Feature.Configurable

Overrides:

describe in class AbstractProjectCommand<Compile.Result>

set

public void set(String option,
                Object value)
         throws wycc.lang.Feature.ConfigurationError

Specified by:

set in interface wycc.lang.Feature.Configurable

Overrides:

set in class AbstractProjectCommand<Compile.Result>

Throws:

wycc.lang.Feature.ConfigurationError

getDescription

public String getDescription()

setVerify

public void setVerify(boolean flag)

getVerify

public boolean getVerify()

setVerificationConditions

public void setVerificationConditions(boolean flag)

getVerificationConditions

public boolean getVerificationConditions()

setVerbose

public void setVerbose()

setVerbose

public void setVerbose(boolean b)

setBrief

public void setBrief()

describeIncludes

public String describeIncludes()

setIncludes

public void setIncludes(wyfs.lang.Content.Filter<WhileyFile> includes)

describeExcludes

public String describeExcludes()

setExcludes

public void setExcludes(wyfs.lang.Content.Filter<WhileyFile> excludes)

execute

public Compile.Result execute(String... args)

execute

public Compile.Result execute(List<? extends wyfs.lang.Path.Entry<?>> entries)

compile

protected Compile.Result compile(wybs.util.StdProject project,
                                 List<? extends wyfs.lang.Path.Entry<?>> entries)

addCompilationBuildRules

protected void addCompilationBuildRules(wybs.util.StdProject project)

Add build rules necessary for compiling whiley source files into binary wyil files.

Parameters:

project -

addWhiley2WyilBuildRule

protected void addWhiley2WyilBuildRule(wybs.util.StdProject project)

Add the rule for compiling Whiley source files into WyIL files.

Parameters:

project -

addVerificationBuildRules

protected void addVerificationBuildRules(wybs.util.StdProject project)

Add build rules necessary for compiling wyil binary files into wyal files for verification.

Parameters:

project -

findCounterexamples

public void findCounterexamples(wyal.lang.WyalFile.Declaration.Assert assertion,
                                wybs.util.StdProject project)

getModifiedSourceFiles

public List getModifiedSourceFiles()
                            throws IOException

Throws:

IOException

getModifiedSourceFiles

public static <T,S> List<wyfs.lang.Path.Entry<T>> getModifiedSourceFiles(wyfs.lang.Path.Root sourceDir,
                                                                         wyfs.lang.Content.Filter<T> sourceIncludes,
                                                                         wyfs.lang.Path.Root binaryDir,
                                                                         wyfs.lang.Content.Type<S> binaryContentType)
                                                                  throws IOException

Generate the list of source files which need to be recompiled. By default, this is done by comparing modification times of each whiley file against its corresponding wyil file. Wyil files which are out-of-date are scheduled to be recompiled.

Returns:

Throws:

IOException