A B C D E F G H I K L M N O P Q R S T U V W

A

AbstractBytecode - Class in wyil.util

AbstractBytecode() - Constructor for class wyil.util.AbstractBytecode

AbstractBytecode(int) - Constructor for class wyil.util.AbstractBytecode

AbstractBytecode(int[]) - Constructor for class wyil.util.AbstractBytecode

AbstractBytecode(int[][]) - Constructor for class wyil.util.AbstractBytecode

AbstractBytecode(int, int[][]) - Constructor for class wyil.util.AbstractBytecode

AbstractBytecode(int[], int[][]) - Constructor for class wyil.util.AbstractBytecode

AbstractBytecode(int, int[][], int[]) - Constructor for class wyil.util.AbstractBytecode

AbstractBytecode(int[], int[][], int[]) - Constructor for class wyil.util.AbstractBytecode

AbstractFunctionOrMethod(String, Collection<WyalFile.Type>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.AbstractFunctionOrMethod

AbstractFunctionOrMethod(String, Collection<WyalFile.Type>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractFunctionOrMethod

AbstractIndirectInvoke(Expr, Collection<Expr>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.AbstractIndirectInvoke

AbstractIndirectInvoke(Expr, Collection<Expr>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractIndirectInvoke

AbstractInvoke(String, Path.ID, Collection<Expr>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.AbstractInvoke

AbstractInvoke(String, Path.ID, Collection<Expr>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractInvoke

AbstractProjectCommand<T> - Class in wyc.util

Provides an abstract command from which other commands for controlling the Whiley compiler can be derived.

AbstractProjectCommand(Content.Registry, Logger) - Constructor for class wyc.util.AbstractProjectCommand

Construct a new instance of this command.

AbstractVariable(String, Attribute...) - Constructor for class wyc.lang.Expr.AbstractVariable

AbstractVariable(String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AbstractVariable

Activator - Class in wyc

Activator() - Constructor for class wyc.Activator

Activator.Registry - Class in wyc

Default implementation of a content registry.

add(WhileyFile.Declaration) - Method in class wyc.lang.WhileyFile

addBootpath(List<Path.Root>) - Method in class wyc.util.AbstractProjectCommand

Initialise the bootpath for use with the compiler.

addCompilationBuildRules(StdProject) - Method in class wyc.commands.Compile

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

addParameters(Collection<String>) - Method in class wyil.util.type.LifetimeRelation

Add a method's lifetime parameters to this relation.

addVerificationBuildRules(StdProject) - Method in class wyc.commands.Compile

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

addWhiley2WyilBuildRule(StdProject) - Method in class wyc.commands.Compile

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

afterType - Variable in class wyc.lang.Expr.AssignedVariable

AliasDeclaration(int) - Constructor for class wyil.lang.Bytecode.AliasDeclaration

ALLOCATION_NOT_PERMITTED - Static variable in class wyil.util.ErrorMessages

AMBIGUOUS_COERCION - Static variable in class wyil.util.ErrorMessages

AntTask - Class in wyc.util

This class implements an baseline ant task for compiling whiley files via ant and an appropriate build.xml file.

AntTask() - Constructor for class wyc.util.AntTask

Construct a new instance of this command.

apply(WyilFile) - Method in class wyil.checks.CoercionCheck

apply(WyilFile) - Method in class wyil.io.WyilFilePrinter

apply(Constant[], Interpreter, SyntaxTree.Location<Bytecode.Operator>) - Method in interface wyil.util.interpreter.Interpreter.InternalFunction

apply(WyilFile) - Method in class wyil.util.MoveAnalysis

applySubstitution(List<String>, List<String>, Type) - Static method in class wyc.builder.FlowTypeChecker

Apply a lifetime substitution: Substitute all parameters in original by their arguments.

argument(int) - Method in class wyil.lang.Bytecode.IndirectInvoke

Return operand holding the ith parameter for the invoked function.

arguments - Variable in class wyc.lang.Expr.AbstractIndirectInvoke

arguments - Variable in class wyc.lang.Expr.AbstractInvoke

arguments - Variable in class wyc.lang.Expr.ArrayInitialiser

arguments() - Method in class wyil.lang.Bytecode.IndirectInvoke

Return operands holding parameters for the invoked function.

arguments() - Method in class wyil.lang.Constant.FunctionOrMethod

ARGUMENTS - Static variable in class wyil.lang.SyntaxTree

Array(Collection<Constant>) - Constructor for class wyil.lang.Constant.Array

Array(Type) - Static method in interface wyil.lang.Type

ArrayGenerator(Expr, Expr, Attribute...) - Constructor for class wyc.lang.Expr.ArrayGenerator

ArrayInitialiser(Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.ArrayInitialiser

ArrayInitialiser(Attribute, Expr...) - Constructor for class wyc.lang.Expr.ArrayInitialiser

arrayToString(int...) - Static method in class wyil.lang.Bytecode.Util

Assert(Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Assert

Create a given assert statement.

Assert(String, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Assert

Create a given assert statement.

Assert(int) - Constructor for class wyil.lang.Bytecode.Assert

Assign(List<Expr.LVal>, List<Expr>, Attribute...) - Constructor for class wyc.lang.Stmt.Assign

Create an assignment from a given sequence of lvals and expressions on the right-hand side.

Assign(List<Expr.LVal>, List<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Assign

Create an assignment from a given sequence of lvals and expressions on the right-hand side.

Assign(int, int) - Constructor for class wyil.lang.Bytecode.Assign

Construct an assignment from a right-hand operand to a left-hand operand.

Assign(int[], int[]) - Constructor for class wyil.lang.Bytecode.Assign

Construct an assignment from a right-hand operand to a left-hand operand.

AssignedVariable(String, Attribute...) - Constructor for class wyc.lang.Expr.AssignedVariable

AssignedVariable(String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.AssignedVariable

associate(Path.Entry) - Method in class wyc.Activator.Registry

Assume(Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Assume

Create a given assume statement.

Assume(String, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Assume

Create a given assume statement.

Assume(int) - Constructor for class wyil.lang.Bytecode.Assume

Atom() - Constructor for class wyil.lang.Type.Impl.Atom

attribute(Class<T>) - Method in class wyil.lang.WyilFile.Block

attributes() - Method in class wyil.lang.WyilFile.Block

Automata - Class in wyautl_old.lang

This class provides various algorithms for manipulating automata.

Automata() - Constructor for class wyautl_old.lang.Automata

Automaton - Class in wyautl_old.lang

A finite-state automaton for representing Whiley types.

Automaton(Automaton.State...) - Constructor for class wyautl_old.lang.Automaton

Automaton(List<Automaton.State>) - Constructor for class wyautl_old.lang.Automaton

Automaton(Automaton) - Constructor for class wyautl_old.lang.Automaton

Automaton.State - Class in wyautl_old.lang

Represents a state in an automaton.

B

BINARY_ASSIGNABLE - Static variable in interface wyil.lang.Bytecode

BINARY_OPERATOR - Static variable in interface wyil.lang.Bytecode

BinaryAutomataWriter - Class in wyautl_old.io

Responsible for writing an automaton in a binary format to an output stream.

BinaryAutomataWriter(BinaryOutputStream) - Constructor for class wyautl_old.io.BinaryAutomataWriter

BinaryMatrix - Class in wyautl_old.util

A binary matrix represents a matrix of binary digits.

BinaryMatrix(int, int, boolean) - Constructor for class wyautl_old.util.BinaryMatrix

Construct an empty binary matrix of a given number of rows and columns.

BinaryTypeWriter - Class in wyil.util.type

A BinaryWriter will write types to a binary output stream.

BinaryTypeWriter(BinaryOutputStream) - Constructor for class wyil.util.type.BinaryTypeWriter

BinOp(Expr.BOp, Expr, Expr, Attribute...) - Constructor for class wyc.lang.Expr.BinOp

BinOp(Expr.BOp, Expr, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Expr.BinOp

Block(int...) - Constructor for class wyil.lang.Bytecode.Block

block() - Method in class wyil.lang.Bytecode.Case

block() - Method in class wyil.lang.Bytecode.Index

Block(WyilFile, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.Block

Block(WyilFile, Attribute[]) - Constructor for class wyil.lang.WyilFile.Block

BLOCK_Constant - Static variable in class wyil.io.WyilFileWriter

BLOCK_Documentation - Static variable in class wyil.io.WyilFileWriter

BLOCK_Function - Static variable in class wyil.io.WyilFileWriter

BLOCK_Header - Static variable in class wyil.io.WyilFileWriter

BLOCK_License - Static variable in class wyil.io.WyilFileWriter

BLOCK_Method - Static variable in class wyil.io.WyilFileWriter

BLOCK_Module - Static variable in class wyil.io.WyilFileWriter

BLOCK_Property - Static variable in class wyil.io.WyilFileWriter

BLOCK_Type - Static variable in class wyil.io.WyilFileWriter

blocks() - Method in class wyil.lang.WyilFile

Returns all declarations declared in this WyilFile.

body - Variable in class wyc.lang.Expr.Lambda

body - Variable in class wyc.lang.Stmt.DoWhile

body - Variable in class wyc.lang.Stmt.NamedBlock

body - Variable in class wyc.lang.Stmt.While

body() - Method in class wyil.lang.Bytecode.Lambda

body() - Method in class wyil.lang.Bytecode.Loop

Return the block identifier of the loop body.

body() - Method in class wyil.lang.Bytecode.Quantifier

BODY - Static variable in class wyil.lang.SyntaxTree

Bool(boolean) - Static method in class wyil.lang.Constant

Get the appropriate Bool constant corresponding to a Java boolean.

bounds() - Method in interface wyil.lang.Type.Intersection

bounds() - Method in interface wyil.lang.Type.Union

BRANCH_ALWAYS_TAKEN - Static variable in class wyil.util.ErrorMessages

Break(Attribute...) - Constructor for class wyc.lang.Stmt.Break

Break() - Constructor for class wyil.lang.Bytecode.Break

BREAK_OUTSIDE_SWITCH_OR_LOOP - Static variable in class wyil.util.ErrorMessages

brief - Variable in class wyc.commands.Compile

Signals that brief error reporting should be used.

build(Collection<Pair<Path.Entry<?>, Path.Root>>, Build.Graph) - Method in class wyc.builder.CompileTask

build(Collection<Pair<Path.Entry<?>, Path.Root>>, Build.Graph) - Method in class wyc.builder.DecompileTask

build(Collection<Pair<Path.Entry<?>, Path.Root>>, Build.Graph) - Method in class wyil.builders.Wyil2WyalBuilder

buildVerificationCondition(WyilFile.FunctionOrMethod, VerificationConditionGenerator.GlobalEnvironment, VerificationConditionGenerator.VerificationCondition) - Method in class wyil.builders.VerificationConditionGenerator

Construct a fully typed and quantified expression for representing a verification condition.

Byte(byte) - Constructor for class wyil.lang.Constant.Byte

Bytecode - Interface in wyil.lang

Each bytecode has a binary format which identifies the opcode, operand registers, operand groups, blocks and other items used (e.g.

Bytecode.AliasDeclaration - Class in wyil.lang

An alias declaration bytecode has the following form:

Bytecode.Assert - Class in wyil.lang

An assert bytecode has the following layout:

Bytecode.AssertOrAssume - Class in wyil.lang

An abstract class representing either an assert or assume bytecode.

Bytecode.Assign - Class in wyil.lang

An assignment bytecode has the following layout:

Bytecode.Assume - Class in wyil.lang

An assume bytecode has the following layout:

Bytecode.Block - Class in wyil.lang

Bytecode.Blocks - Enum in wyil.lang

Bytecode.Break - Class in wyil.lang

A break bytecode has the following layout:

Bytecode.Case - Class in wyil.lang

Bytecode.Const - Class in wyil.lang

A constant bytecode has the following layout:

Bytecode.Continue - Class in wyil.lang

A continue bytecode has the following layout:

Bytecode.Convert - Class in wyil.lang

A convert bytecode has the following layout:

Bytecode.Debug - Class in wyil.lang

A debug bytecode has the following layout:

Bytecode.DoWhile - Class in wyil.lang

A Do While bytecode has the same format as the underlying loop bytecode.

Bytecode.Expr - Interface in wyil.lang

Represents the class of bytecodes which correspond to expressions in the source language.

Bytecode.Extras - Enum in wyil.lang

Bytecode.Fail - Class in wyil.lang

A panic bytecode has the following layout:

Bytecode.FieldLoad - Class in wyil.lang

A field load bytecode has the following layout:

Bytecode.If - Class in wyil.lang

An if bytecode has one of the the following layouts:

Bytecode.Index - Class in wyil.lang

Represents a bytecode location within a code forest.

Bytecode.IndirectInvoke - Class in wyil.lang

An indirect invocation bytecode has the following layout:

Bytecode.Invoke - Class in wyil.lang

An indirect invocation bytecode has the following layout:

Bytecode.Lambda - Class in wyil.lang

A lambda bytecode has the following layout:

Bytecode.Loop - Class in wyil.lang

A loop bytecode has the following layout:

Bytecode.NamedBlock - Class in wyil.lang

Bytecode.OperandGroups - Enum in wyil.lang

Bytecode.Operands - Enum in wyil.lang

Bytecode.Operator - Class in wyil.lang

An operator bytecode has the following layout:

Bytecode.OperatorKind - Enum in wyil.lang

Represents the set of valid operators (e.g.

Bytecode.Quantifier - Class in wyil.lang

A quantifier bytecode has the following layout:

Bytecode.QuantifierKind - Enum in wyil.lang

Bytecode.Range - Class in wyil.lang

Bytecode.Return - Class in wyil.lang

A return bytecode has the following layout:

Bytecode.Schema - Class in wyil.lang

Bytecode.Skip - Class in wyil.lang

A skip bytecode has the following layout:

Bytecode.Stmt - Interface in wyil.lang

A statement bytecode represents a bytecode that contains a sequence of zero or more bytecodes.

Bytecode.StmtExpr - Interface in wyil.lang

A "statement expression" is a rather unusual beast.

Bytecode.Switch - Class in wyil.lang

A switch bytecode has the following layout:

Bytecode.Util - Class in wyil.lang

Bytecode.VariableAccess - Class in wyil.lang

A variable access bytecode represents a specific read of a given variable.

Bytecode.VariableDeclaration - Class in wyil.lang

A variable declaration bytecode has one of the following two layouts:

Bytecode.While - Class in wyil.lang

A While bytecode has the same format as the underlying loop bytecode.

C

Case(List<Expr>, List<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.Case

Case(int, Constant...) - Constructor for class wyil.lang.Bytecode.Case

Case(int, List<Constant>) - Constructor for class wyil.lang.Bytecode.Case

cases - Variable in class wyc.lang.Stmt.Switch

cases() - Method in class wyil.lang.Bytecode.Switch

Cast(WyalFile.Type, Expr, Attribute...) - Constructor for class wyc.lang.Expr.Cast

check() - Method in class wyc.builder.DefiniteAssignmentAnalysis

check() - Method in class wyc.builder.ModuleCheck

check(WhileyFile.Declaration) - Method in class wyc.builder.ModuleCheck

check(SyntaxTree) - Method in class wyil.checks.CoercionCheck

check(Type, Type, HashSet<Pair<Type, Type>>, SyntacticElement) - Method in class wyil.checks.CoercionCheck

Recursively check that there is no ambiguity in coercing type from into type to.

checkInvariants(Constant[], List<SyntaxTree.Location<Bytecode.Expr>>) - Method in class wyil.util.interpreter.Interpreter

Evaluate zero or more conditional expressions, and check whether any is false.

checkInvariants(Constant[], SyntaxTree.Location<Bytecode.Expr>...) - Method in class wyil.util.interpreter.Interpreter

Evaluate zero or more conditional expressions, and check whether any is false.

checkType(Constant, SyntacticElement, Class<T>...) - Static method in class wyil.util.interpreter.Interpreter

Check that a given operand value matches an expected type.

children - Variable in class wyautl_old.lang.Automaton.State

close() - Method in class wyautl_old.io.BinaryAutomataWriter

close() - Method in interface wyautl_old.io.GenericWriter

close() - Method in class wyil.io.WyilFileReader

close() - Method in class wyil.io.WyilFileWriter

CodeGenerator - Class in wyc.builder

Responsible for compiling the declarations, statements and expression found in a WhileyFile into WyIL declarations and bytecode blocks.

CodeGenerator(CompileTask) - Constructor for class wyc.builder.CodeGenerator

Construct a code generator object for translating WhileyFiles into WyilFiles.

CoercionCheck - Class in wyil.checks

The point of the coercion check is to check that all convert bytecodes make sense, and are not ambiguous.

CoercionCheck(Build.Task) - Constructor for class wyil.checks.CoercionCheck

command - Variable in class wyc.util.AntTask

compare(String, String) - Static method in class wyc.util.TestUtils

Compare the output of executing java on the test case with a reference file.

compareTo(Constant) - Method in class wyil.lang.Constant.Array

compareTo(Constant) - Method in class wyil.lang.Constant.Bool

compareTo(Constant) - Method in class wyil.lang.Constant.Byte

compareTo(Constant) - Method in class wyil.lang.Constant.FunctionOrMethod

compareTo(Constant) - Method in class wyil.lang.Constant.Integer

compareTo(Constant) - Method in class wyil.lang.Constant.Null

compareTo(Constant) - Method in class wyil.lang.Constant.Record

compareTo(Constant) - Method in class wyil.lang.Constant.Type

compareTo(Type.Impl) - Method in class wyil.lang.Type.Impl.FunctionOrMethod

compareTo(Type.Impl) - Method in class wyil.lang.Type.Impl.Primitive

compareTo(Constant) - Method in class wyil.util.interpreter.Interpreter.ConstantLambda

compareTo(Constant) - Method in class wyil.util.interpreter.Interpreter.ConstantObject

compareTo(TypeSystem.FunctionOrMethodState) - Method in class wyil.util.TypeSystem.FunctionOrMethodState

Compile - Class in wyc.commands

Compile(Content.Registry, Logger) - Constructor for class wyc.commands.Compile

Construct a new instance of this command.

Compile(Content.Registry, Logger, OutputStream, OutputStream) - Constructor for class wyc.commands.Compile

Construct a new instance of this command.

compile(StdProject, List<? extends Path.Entry<?>>) - Method in class wyc.commands.Compile

compile(File, boolean, String...) - Static method in class wyc.util.TestUtils

Run the Whiley Compiler with the given list of arguments.

Compile.Result - Enum in wyc.commands

Result kind for this command

CompileTask - Class in wyc.builder

Responsible for managing the process of turning source files into binary code for execution.

CompileTask(Build.Project) - Constructor for class wyc.builder.CompileTask

condition - Variable in class wyc.lang.Expr.Quantifier

condition - Variable in class wyc.lang.Stmt.DoWhile

condition - Variable in class wyc.lang.Stmt.IfElse

condition - Variable in class wyc.lang.Stmt.While

condition() - Method in class wyil.lang.Bytecode.If

condition() - Method in class wyil.lang.Bytecode.Loop

Return the loop condition operand.

CONDITION - Static variable in class wyil.lang.SyntaxTree

Some helpful context to make reading the code using syntax trees simpler.

Conjunctable() - Constructor for class wyil.lang.Type.Impl.Conjunctable

Const(Constant) - Constructor for class wyil.lang.Bytecode.Const

Constant(Constant, Attribute...) - Constructor for class wyc.lang.Expr.Constant

Constant(List<Modifier>, Expr, String, Attribute...) - Constructor for class wyc.lang.WhileyFile.Constant

constant - Variable in class wyc.lang.WhileyFile.Constant

constant() - Method in class wyil.lang.Bytecode.Const

Constant - Class in wyil.lang

Constant() - Constructor for class wyil.lang.Constant

constant(String) - Method in class wyil.lang.WyilFile

Looks up a constant declaration in this WyilFile with the given name; if none exists, returns null.

Constant(WyilFile, Collection<Modifier>, String, Constant, Attribute...) - Constructor for class wyil.lang.WyilFile.Constant

Constant(WyilFile, Collection<Modifier>, String, Constant, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.Constant

constant() - Method in class wyil.lang.WyilFile.Constant

Constant.Array - Class in wyil.lang

Constant.Bool - Class in wyil.lang

Constant.Byte - Class in wyil.lang

Constant.FunctionOrMethod - Class in wyil.lang

Represents a named function or method.

Constant.Integer - Class in wyil.lang

Constant.Null - Class in wyil.lang

Constant.Record - Class in wyil.lang

Constant.Type - Class in wyil.lang

CONSTANT_Array - Static variable in class wyil.io.WyilFileWriter

CONSTANT_Byte - Static variable in class wyil.io.WyilFileWriter

CONSTANT_False - Static variable in class wyil.io.WyilFileWriter

CONSTANT_Function - Static variable in class wyil.io.WyilFileWriter

CONSTANT_Int - Static variable in class wyil.io.WyilFileWriter

CONSTANT_Method - Static variable in class wyil.io.WyilFileWriter

CONSTANT_Null - Static variable in class wyil.io.WyilFileWriter

CONSTANT_Record - Static variable in class wyil.io.WyilFileWriter

CONSTANT_True - Static variable in class wyil.io.WyilFileWriter

CONSTANT_Type - Static variable in class wyil.io.WyilFileWriter

ConstantAccess(String, Path.ID, Attribute...) - Constructor for class wyc.lang.Expr.ConstantAccess

ConstantAccess(String, Path.ID, Collection<Attribute>) - Constructor for class wyc.lang.Expr.ConstantAccess

ConstantLambda(SyntaxTree.Location<Bytecode.Lambda>, Constant...) - Constructor for class wyil.util.interpreter.Interpreter.ConstantLambda

ConstantObject(Constant) - Constructor for class wyil.util.interpreter.Interpreter.ConstantObject

constants - Variable in class wyc.lang.Stmt.Case

constants() - Method in class wyil.lang.WyilFile

Returns all constant declarations in this WyilFile.

construct(int, int[], int[][], int[], Object[]) - Method in class wyil.lang.Bytecode.Schema

ContentType - Static variable in class wyc.lang.WhileyFile

ContentType - Static variable in class wyil.lang.WyilFile

Responsible for identifying and reading/writing WyilFiles.

contextLifetimes - Variable in class wyc.lang.Expr.Lambda

contextLifetimes - Variable in class wyil.lang.Type.Impl.Method

contextLifetimes() - Method in class wyil.lang.Type.Impl.Method

Get the context lifetimes of this function or method type.

contextLifetimes() - Method in interface wyil.lang.Type.Method

Get the context lifetimes for this method.

contextLifetimes - Variable in class wyil.util.TypeSystem.FunctionOrMethodState

Continue(Attribute...) - Constructor for class wyc.lang.Stmt.Continue

Continue() - Constructor for class wyil.lang.Bytecode.Continue

CONTINUE_OUTSIDE_LOOP - Static variable in class wyil.util.ErrorMessages

Convert(int) - Constructor for class wyil.lang.Bytecode.Convert

cop - Variable in class wyc.lang.Expr.Quantifier

count - Variable in class wyc.lang.Expr.ArrayGenerator

counterexamples - Variable in class wyc.commands.Compile

Signals that counterexample generation should be performed.

CYCLIC_CONSTANT_DECLARATION - Static variable in class wyil.util.ErrorMessages

D

data - Variable in class wyautl_old.lang.Automaton.State

DATA_COMPARATOR - Static variable in class wyil.util.type.TypeAlgorithms

The data comparator is used in the type canonicalisation process.

DEAD_CODE - Static variable in class wyil.util.ErrorMessages

Debug(Expr, Attribute...) - Constructor for class wyc.lang.Stmt.Debug

Debug(Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Debug

Debug(int) - Constructor for class wyil.lang.Bytecode.Debug

declaration(String) - Method in class wyc.lang.WhileyFile

Declaration(WyilFile, String, Collection<Modifier>, Attribute...) - Constructor for class wyil.lang.WyilFile.Declaration

Declaration(WyilFile, String, Collection<Modifier>, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.Declaration

declarations - Variable in class wyc.lang.WhileyFile

declarations(Class<T>) - Method in class wyc.lang.WhileyFile

declarations(Class<T>, String) - Method in class wyc.lang.WhileyFile

Decompile - Class in wyc.commands

Decompile(Content.Registry, Logger) - Constructor for class wyc.commands.Decompile

Decompile.Result - Enum in wyc.commands

Result kind for this command

DecompileTask - Class in wyc.builder

Responsible for decompiling WyIL files into a human readable form.

DecompileTask(Build.Project) - Constructor for class wyc.builder.DecompileTask

DefiniteAssignmentAnalysis - Class in wyc.builder

Responsible for checking that all variables are defined before they are used.

DefiniteAssignmentAnalysis(WhileyFile) - Constructor for class wyc.builder.DefiniteAssignmentAnalysis

Dereference(Expr, Attribute...) - Constructor for class wyc.lang.Expr.Dereference

describe(String) - Method in class wyc.commands.Compile

describe(String) - Method in class wyc.util.AbstractProjectCommand

describeExcludes() - Method in class wyc.commands.Compile

describeIncludes() - Method in class wyc.commands.Compile

describeVerbose() - Method in class wyc.commands.Decompile

determineUsedVariables(SyntaxTree.Location<?>...) - Static method in class wyil.util.SyntaxTrees

Traverse a syntax tree from one or more roots looking for variable accesses (uses).

deterministic - Variable in class wyautl_old.lang.Automaton.State

DoWhile(Expr, List<Expr>, Collection<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.DoWhile

Construct a Do-While statement from a given condition and body of statements.

DoWhile(Expr, List<Expr>, Collection<Stmt>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.DoWhile

Construct a Do-While statement from a given condition and body of statements.

DoWhile(int, int, int[], int[]) - Constructor for class wyil.lang.Bytecode.DoWhile

DUPLICATE_CASE_LABEL - Static variable in class wyil.util.ErrorMessages

DUPLICATE_DEFAULT_LABEL - Static variable in class wyil.util.ErrorMessages

E

element - Variable in class wyc.lang.Expr.ArrayGenerator

element() - Method in interface wyil.lang.Type.Array

Get the element type of this array.

element() - Method in interface wyil.lang.Type.Negation

Get the element type of this array.

element() - Method in interface wyil.lang.Type.Reference

Return the type of the location that this reference refers to.

EMPTY - Static variable in class wyil.util.type.LifetimeRelation

end() - Method in class wyc.io.WhileyFileLexer.Token

END - Static variable in class wyil.lang.SyntaxTree

endNamedBlock(String) - Method in class wyil.util.type.LifetimeRelation

Remove the named block with the given name from this relation.

endOperand() - Method in class wyil.lang.Bytecode.Range

Return the end operand of this range.

ensures - Variable in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

environment() - Method in class wyil.lang.Bytecode.Lambda

ENVIRONMENT - Static variable in class wyil.lang.SyntaxTree

equals(Object) - Method in class wyautl_old.lang.Automaton

This method compares two compound types to test whether they are identical.

equals(Object) - Method in class wyautl_old.lang.Automaton.State

equals(Object) - Method in class wyil.lang.Bytecode.Case

equals(Object) - Method in class wyil.lang.Bytecode.Const

equals(Object) - Method in class wyil.lang.Bytecode.FieldLoad

equals(Object) - Method in class wyil.lang.Bytecode.Index

equals(Object) - Method in class wyil.lang.Bytecode.IndirectInvoke

equals(Object) - Method in class wyil.lang.Bytecode.Invoke

equals(Object) - Method in class wyil.lang.Bytecode.Lambda

equals(Object) - Method in class wyil.lang.Bytecode.NamedBlock

equals(Object) - Method in class wyil.lang.Bytecode.Range

equals(Object) - Method in class wyil.lang.Bytecode.Switch

equals(Object) - Method in class wyil.lang.Bytecode.VariableDeclaration

equals(Object) - Method in class wyil.lang.Constant.Array

equals(Object) - Method in class wyil.lang.Constant.Bool

equals(Object) - Method in class wyil.lang.Constant.Byte

equals(Object) - Method in class wyil.lang.Constant.FunctionOrMethod

equals(Object) - Method in class wyil.lang.Constant.Integer

equals(Object) - Method in class wyil.lang.Constant.Null

equals(Object) - Method in class wyil.lang.Constant.Record

equals(Object) - Method in class wyil.lang.Constant.Type

equals(Object) - Method in class wyil.lang.Type.Impl.FunctionOrMethod

equals(Object) - Method in class wyil.lang.Type.Impl.Method

equals(Object) - Method in class wyil.lang.Type.Impl.Primitive

equals(Object) - Method in class wyil.util.AbstractBytecode

equals(Object) - Method in class wyil.util.interpreter.Interpreter.ConstantLambda

equals(Object) - Method in class wyil.util.interpreter.Interpreter.ConstantObject

equals(Object) - Method in class wyil.util.TypeSystem.FunctionOrMethodState

equals(Object) - Method in class wyil.util.TypeSystem.RecordState

error(String, SyntacticElement) - Static method in class wyil.util.interpreter.Interpreter

This method is provided as a generic mechanism for reporting runtime errors within the interpreter.

errorMessage(ErrorMessages.MsgWithNoParams) - Static method in class wyil.util.ErrorMessages

Return the error message for an error with no parameters.

errorMessage(ErrorMessages.MsgWithStringParam, String) - Static method in class wyil.util.ErrorMessages

Return the error message for an error with a single string parameter.

errorMessage(ErrorMessages.MsgWithTypeParam, Type) - Static method in class wyil.util.ErrorMessages

Return the error message for an error with a single type parameter.

errorMessage(ErrorMessages.MsgWithTypeParams, Type, Type) - Static method in class wyil.util.ErrorMessages

Return the error message for an error with two type parameters.

ErrorMessages - Class in wyil.util

Contains global constants mapping syntax errors to their error messages.

ErrorMessages() - Constructor for class wyil.util.ErrorMessages

execute(String...) - Method in class wyc.commands.Compile

execute(List<? extends Path.Entry<?>>) - Method in class wyc.commands.Compile

execute(String...) - Method in class wyc.commands.Decompile

execute(String...) - Method in class wyc.commands.Run

execute() - Method in class wyc.util.AntTask

execute(NameID, Type.FunctionOrMethod, Constant...) - Method in class wyil.util.interpreter.Interpreter

Execute a function or method identified by a name and type signature with the given arguments, producing a return value or null (if none).

execWyil(File, Path.ID) - Static method in class wyc.util.TestUtils

Execute a given WyIL file using the default interpreter.

exists(Path.ID) - Method in class wyc.builder.CompileTask

expandAsEffectiveArray(Expr, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsEffectiveArray(Type, SyntacticElement, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsEffectiveArray(Type) - Method in class wyil.util.TypeSystem

Assuming given type is an effective array of some sort, expand to ensure array structure is visible.

expandAsEffectiveFunctionOrMethod(Expr, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsEffectiveFunctionOrMethod(Type, SyntacticElement, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsEffectiveRecord(Expr, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsEffectiveRecord(Type, SyntacticElement, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsEffectiveRecord(Type) - Method in class wyil.util.TypeSystem

Assuming given type is an effective record of some sort, expand to ensure record structure is visible.

expandAsEffectiveReference(Expr, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsEffectiveReference(Type, SyntacticElement, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

expandAsFunctionOrMethod(Type) - Method in class wyil.util.TypeSystem

Assuming given type is an effective function or method type of some sort, expand to ensure structure is visible.

expandAsReference(Type) - Method in class wyil.util.TypeSystem

Assuming given type is an effective reference of some sort, expand to ensure reference structure is visible.

expandOneLevel(Type) - Method in class wyil.util.TypeSystem

Expand a given syntactic type by exactly one level.

ExplicitCoercionOperator - Class in wyil.util.type

The explicit coercion operator extends the implicit coercion operator to include coercions which must be specified with an explicit cast operation.

ExplicitCoercionOperator(Automaton, Automaton, LifetimeRelation) - Constructor for class wyil.util.type.ExplicitCoercionOperator

EXPORT - Static variable in interface wyil.lang.Modifier

Expr - Interface in wyc.lang

Provides classes for representing expressions in Whiley's source language.

expr - Variable in class wyc.lang.Expr.Cast

expr - Variable in class wyc.lang.Expr.New

expr - Variable in class wyc.lang.Stmt.Assert

expr - Variable in class wyc.lang.Stmt.Assume

expr - Variable in class wyc.lang.Stmt.Case

expr - Variable in class wyc.lang.Stmt.Debug

expr - Variable in class wyc.lang.Stmt.Switch

expr - Variable in class wyc.lang.Stmt.VariableDeclaration

Expr.AbstractFunctionOrMethod - Class in wyc.lang

Expr.AbstractIndirectInvoke - Class in wyc.lang

Expr.AbstractInvoke - Class in wyc.lang

Expr.AbstractVariable - Class in wyc.lang

Expr.ArrayGenerator - Class in wyc.lang

Represents an array generator expression, which is of the form:

Expr.ArrayInitialiser - Class in wyc.lang

Represents an array initialiser expression, which is of the form:

Expr.AssignedVariable - Class in wyc.lang

Expr.BinOp - Class in wyc.lang

Expr.BOp - Enum in wyc.lang

Expr.Cast - Class in wyc.lang

Represents a cast expression, which has the form:

Expr.Constant - Class in wyc.lang

Expr.ConstantAccess - Class in wyc.lang

Expr.Dereference - Class in wyc.lang

Expr.FieldAccess - Class in wyc.lang

Expr.FunctionCall - Class in wyc.lang

Parse a function invocation expression, which has the form:

Expr.FunctionOrMethod - Class in wyc.lang

Expr.FunctionOrMethodCall - Class in wyc.lang

Expr.IndexOf - Class in wyc.lang

Expr.IndirectFunctionCall - Class in wyc.lang

Expr.IndirectFunctionOrMethodCall - Class in wyc.lang

Expr.IndirectMethodCall - Class in wyc.lang

Expr.Lambda - Class in wyc.lang

Expr.LocalVariable - Class in wyc.lang

Expr.LVal - Interface in wyc.lang

An LVal is a special form of expression which may appear on the left-hand side of an assignment.

Expr.MethodCall - Class in wyc.lang

Expr.Multi - Interface in wyc.lang

A Multi expression is one which returns multiple values.

Expr.New - Class in wyc.lang

Expr.PropertyCall - Class in wyc.lang

Expr.QOp - Enum in wyc.lang

Expr.Quantifier - Class in wyc.lang

Expr.Record - Class in wyc.lang

Expr.TypeVal - Class in wyc.lang

Expr.UnOp - Class in wyc.lang

Expr.UOp - Enum in wyc.lang

Exprs - Class in wyc.lang

Exprs() - Constructor for class wyc.lang.Exprs

extract(Automaton, int) - Static method in class wyautl_old.lang.Automata

Traverse the automaton rooted at the given state and recursively extract all reachable states to produce a (potentially smaller) automaton.

extractOnto(int, Automaton, ArrayList<Automaton.State>) - Static method in class wyautl_old.lang.Automata

extras() - Method in class wyil.lang.Bytecode.Schema

F

Fail(Attribute...) - Constructor for class wyc.lang.Stmt.Fail

Fail() - Constructor for class wyil.lang.Bytecode.Fail

False - Static variable in class wyil.lang.Constant

The Bool false constant

falseBranch - Variable in class wyc.lang.Stmt.IfElse

falseBranch() - Method in class wyil.lang.Bytecode.If

Return the block identifier for the false branch associated with this bytecode.

FALSEBRANCH - Static variable in class wyil.lang.SyntaxTree

FieldAccess(Expr, String, Attribute...) - Constructor for class wyc.lang.Expr.FieldAccess

FieldAccess(Expr, String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.FieldAccess

FieldLoad(int, String) - Constructor for class wyil.lang.Bytecode.FieldLoad

fieldName() - Method in class wyil.lang.Bytecode.FieldLoad

fields - Variable in class wyc.lang.Expr.Record

file() - Method in interface wyc.lang.WhileyFile.Context

filter - Variable in class wyc.lang.WhileyFile.Import

finaliseConfiguration() - Method in class wyc.util.AbstractProjectCommand

Finalise the given configuration to ensure it is an consistent state.

findCounterexamples(WyalFile.Declaration.Assert, StdProject) - Method in class wyc.commands.Compile

findTestNames(String) - Static method in class wyc.util.TestUtils

Scan a directory to get the names of all the whiley source files in that directory.

flattern(int[][]) - Static method in class wyil.builders.VerificationConditionGenerator

FlowTypeChecker - Class in wyc.builder

Propagates type information in a flow-sensitive fashion from declared parameter and return types through variable declarations and assigned expressions, to determine types for all intermediate expressions and variables.

FlowTypeChecker(CompileTask) - Constructor for class wyc.builder.FlowTypeChecker

flush() - Method in class wyautl_old.io.BinaryAutomataWriter

flush() - Method in interface wyautl_old.io.GenericWriter

freeVariables(SyntacticItem, Set<WyalFile.VariableDeclaration>) - Method in class wyil.builders.VerificationConditionGenerator

Determine all free variables which are used within the given expression.

freshLabel() - Static method in class wyc.builder.CodeGenerator

from - Variable in class wyil.util.type.SubtypeOperator

fromString(String) - Static method in interface wyil.lang.Type

Function(List<Modifier>, String, List<WhileyFile.Parameter>, List<WhileyFile.Parameter>, List<Expr>, List<Expr>, List<Stmt>, Attribute...) - Constructor for class wyc.lang.WhileyFile.Function

Function(Type[], Type[]) - Static method in interface wyil.lang.Type

Function(Type.Impl[], Type.Impl[]) - Constructor for class wyil.lang.Type.Impl.Function

FUNCTION_OR_METHOD_TYPE_REQUIRED - Static variable in class wyil.util.ErrorMessages

FunctionCall(NameID, Path.ID, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.FunctionCall

FunctionCall(NameID, Path.ID, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.FunctionCall

FunctionOrMethod(NameID, Collection<WyalFile.Type>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.FunctionOrMethod

FunctionOrMethod(NameID, Collection<WyalFile.Type>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.FunctionOrMethod

FunctionOrMethod(NameID, Type.FunctionOrMethod, Constant...) - Constructor for class wyil.lang.Constant.FunctionOrMethod

FunctionOrMethod(NameID, Type.FunctionOrMethod, Collection<Constant>) - Constructor for class wyil.lang.Constant.FunctionOrMethod

FunctionOrMethod(Type.Impl[], Type.Impl[]) - Constructor for class wyil.lang.Type.Impl.FunctionOrMethod

FunctionOrMethod(WyilFile, Collection<Modifier>, String, Type.FunctionOrMethod, Attribute...) - Constructor for class wyil.lang.WyilFile.FunctionOrMethod

FunctionOrMethod(WyilFile, Collection<Modifier>, String, Type.FunctionOrMethod, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.FunctionOrMethod

FunctionOrMethodCall(NameID, Path.ID, Collection<Expr>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.FunctionOrMethodCall

FunctionOrMethodCall(NameID, Path.ID, Collection<Expr>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.FunctionOrMethodCall

FunctionOrMethodOrProperty(List<Modifier>, String, List<WhileyFile.Parameter>, List<WhileyFile.Parameter>, List<String>, List<Expr>, List<Expr>, List<Stmt>, Attribute...) - Constructor for class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

Construct an object representing a Whiley function.

functionOrMethodOrProperty(String) - Method in class wyil.lang.WyilFile

Returns all function or method declarations in this WyilFile with the given name.

functionOrMethodOrProperty(String, Type.FunctionOrMethod) - Method in class wyil.lang.WyilFile

Looks up a function or method declaration in this WyilFile with the given name and type; if none exists, returns null.

FunctionOrMethodOrProperty(WyilFile, Collection<Modifier>, String, Type.FunctionOrMethod, Attribute...) - Constructor for class wyil.lang.WyilFile.FunctionOrMethodOrProperty

FunctionOrMethodOrProperty(WyilFile, Collection<Modifier>, String, Type.FunctionOrMethod, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.FunctionOrMethodOrProperty

functionOrMethods() - Method in class wyil.lang.WyilFile

Returns all function or method declarations in this WyilFile.

FunctionOrMethodState(int, String[], String[]) - Constructor for class wyil.util.TypeSystem.FunctionOrMethodState

functionType - Variable in class wyc.lang.Expr.FunctionCall

functionType - Variable in class wyc.lang.Expr.IndirectFunctionCall

G

generate(WhileyFile, Path.Entry<WyilFile>) - Method in class wyc.builder.CodeGenerator

Generate a WyilFile from a given WhileyFile by translating all of the declarations, statements and expressions into WyIL declarations and bytecode blocks.

generateAndCondition(Expr.BinOp, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Translate a source-level conjunction into a sequence of WyIL bytecodes.

generateAsStmt(Expr.FunctionOrMethodCall, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Generate an invoke expression as a statement.

generateAsStmt(Expr.IndirectFunctionOrMethodCall, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Generate an indirect invoke expression as a statement.

generateCondition(Expr, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Translate a source-level conditional expression into WyIL bytecodes, using a given scope mapping named variables to locations.

generateExpression(Expr, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Translate a source-level expression into a WYIL bytecode block, using a given environment mapping named variables to registers.

generateFunctionOrMethodCall(Expr.FunctionOrMethodCall, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

generateIndirectFunctionOrMethodCall(Expr.IndirectFunctionOrMethodCall, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

generateIsCondition(Expr.BinOp, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Translate a source-level type test.

generateMultipleReturns(List<Expr>, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Translate a source-level expression into a WyIL bytecode block, using a given environment mapping named variables to registers.

generateNotCondition(Expr.UnOp, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

generateOrCondition(Expr.BinOp, CodeGenerator.EnclosingScope) - Method in class wyc.builder.CodeGenerator

Translate a source-level disjunction into a sequence of WyIL bytecodes.

GenericWriter<T> - Interface in wyautl_old.io

An interface for writing out specific values to a binary stream.

get(int, int) - Method in class wyautl_old.util.BinaryMatrix

get(String) - Method in class wyc.util.AbstractProjectCommand

getAbstractRoot(Path.Root) - Method in class wyc.util.AbstractProjectCommand

Construct a root which is either virtual or corresponds to a physical directory.

getBlock(int) - Method in interface wyil.lang.Bytecode.Stmt

Get the ith block contained in this statement

getBlock(int) - Method in class wyil.lang.SyntaxTree.Location

Get the ith block contained in this statement.

getBlock(int) - Method in class wyil.util.AbstractBytecode

Get the ith block contained in this statement

getBlocks() - Method in class wyil.lang.Bytecode.Schema

getBlocks() - Method in interface wyil.lang.Bytecode.Stmt

Get the blocks contained in this statement

getBlocks() - Method in class wyil.util.AbstractBytecode

Get the blocks contained in this statement

getBody() - Method in class wyil.lang.WyilFile.FunctionOrMethod

Get the body of this function or method

getBytecode() - Method in class wyil.lang.SyntaxTree.Location

Get the bytecode associated with this location

getDescription() - Method in class wyc.commands.Compile

getDescription() - Method in class wyc.commands.Decompile

getDescription() - Method in class wyc.commands.Run

getDirectoryRoot(DirectoryRoot, DirectoryRoot) - Method in class wyc.util.AbstractProjectCommand

Construct a root which must correspond to a physical directory.

getEnclosingDeclaration() - Method in class wyil.lang.SyntaxTree

Get the enclosing declaration of this syntax tree.

getEnclosingTree() - Method in class wyil.lang.SyntaxTree.Location

Get the enclosing syntax tree of this location.

getField(String) - Method in interface wyil.lang.Type.Record

Get the type of a given field in this record

getFieldIndex(String) - Method in interface wyil.lang.Type.EffectiveRecord

Determine the index of a given field in this effective record.

getFieldNames() - Method in interface wyil.lang.Type.EffectiveRecord

Get the array of fields used in this type.

getIndex() - Method in class wyil.lang.SyntaxTree.Location

Get the index of this location in the enclosing syntax tree.

getIndexOf(SyntaxTree.Location<?>) - Method in class wyil.lang.SyntaxTree

Get the index of a given location in this tree.

getInvariant() - Method in class wyil.lang.WyilFile.Type

Get the list of expressions that make up the invariant of this type.

getKind() - Method in class wyil.lang.Type.Impl.Function

getKind() - Method in class wyil.lang.Type.Impl

getKind() - Method in class wyil.lang.Type.Impl.Method

getKind() - Method in class wyil.lang.Type.Impl.Primitive

getKind() - Method in class wyil.lang.Type.Impl.Property

getLocation(int) - Method in class wyil.lang.SyntaxTree

Get the location at a given index in this syntax tree.

getLocations(int...) - Method in class wyil.lang.SyntaxTree

Get the location at a given index in this syntax tree.

getLocations() - Method in class wyil.lang.SyntaxTree

getModifiedSourceFiles() - Method in class wyc.commands.Compile

getModifiedSourceFiles(Path.Root, Content.Filter<T>, Path.Root, Content.Type<S>) - Static method in class wyc.commands.Compile

Generate the list of source files which need to be recompiled.

getModule(Path.ID) - Method in class wyc.builder.CompileTask

Get the (compiled) module associated with a given module identifier.

getName() - Method in class wyc.commands.Compile

getName() - Method in class wyc.commands.Decompile

getName() - Method in class wyc.commands.Run

getName() - Method in class wyil.lang.Bytecode.NamedBlock

getName() - Method in class wyil.lang.Bytecode.VariableDeclaration

getOpcode() - Method in class wyil.lang.Bytecode.AliasDeclaration

getOpcode() - Method in class wyil.lang.Bytecode.Assert

getOpcode() - Method in class wyil.lang.Bytecode.Assign

getOpcode() - Method in class wyil.lang.Bytecode.Assume

getOpcode() - Method in class wyil.lang.Bytecode.Block

getOpcode() - Method in class wyil.lang.Bytecode.Break

getOpcode() - Method in class wyil.lang.Bytecode.Const

getOpcode() - Method in class wyil.lang.Bytecode.Continue

getOpcode() - Method in class wyil.lang.Bytecode.Convert

getOpcode() - Method in class wyil.lang.Bytecode.Debug

getOpcode() - Method in class wyil.lang.Bytecode.DoWhile

getOpcode() - Method in class wyil.lang.Bytecode.Fail

getOpcode() - Method in class wyil.lang.Bytecode.FieldLoad

getOpcode() - Method in interface wyil.lang.Bytecode

Return the opcode value of this bytecode.

getOpcode() - Method in class wyil.lang.Bytecode.If

getOpcode() - Method in class wyil.lang.Bytecode.IndirectInvoke

getOpcode() - Method in class wyil.lang.Bytecode.Invoke

getOpcode() - Method in class wyil.lang.Bytecode.Lambda

getOpcode() - Method in class wyil.lang.Bytecode.NamedBlock

getOpcode() - Method in class wyil.lang.Bytecode.Operator

getOpcode() - Method in class wyil.lang.Bytecode.Quantifier

getOpcode() - Method in class wyil.lang.Bytecode.Return

getOpcode() - Method in class wyil.lang.Bytecode.Skip

getOpcode() - Method in class wyil.lang.Bytecode.Switch

getOpcode() - Method in class wyil.lang.Bytecode.VariableAccess

getOpcode() - Method in class wyil.lang.Bytecode.VariableDeclaration

getOpcode() - Method in class wyil.lang.Bytecode.While

getOpcode() - Method in class wyil.lang.SyntaxTree.Location

Get the underlying opcode for this location

getOpcode() - Method in class wyil.util.AbstractBytecode

Return the opcode value of this bytecode.

getOperand(int) - Method in interface wyil.lang.Bytecode

Return the ith top-level operand in this bytecode.

getOperand(int) - Method in class wyil.lang.SyntaxTree.Location

Return the ith operand associated with this location.

getOperand(int) - Method in class wyil.util.AbstractBytecode

Return the ith top-level operand in this bytecode.

getOperandGroup(int) - Method in interface wyil.lang.Bytecode

Get the ith operand group in this bytecode

getOperandGroup(int) - Method in class wyil.lang.SyntaxTree.Location

Get the ith operand group in this location.

getOperandGroup(int) - Method in class wyil.util.AbstractBytecode

Get the ith operand group in this bytecode

getOperandGroups() - Method in class wyil.lang.Bytecode.Schema

getOperands() - Method in interface wyil.lang.Bytecode

Return the top-level operands in this bytecode.

getOperands() - Method in class wyil.lang.Bytecode.Schema

getOperands() - Method in class wyil.lang.SyntaxTree.Location

Return the ith operand associated with this location.

getOperands() - Method in class wyil.util.AbstractBytecode

Return the top-level operands in this bytecode.

getOptions() - Method in class wyc.commands.Compile

getOptions() - Method in class wyc.util.AbstractProjectCommand

getPostcondition() - Method in class wyil.lang.WyilFile.FunctionOrMethod

Get the list of expressions that make up the postcondition of this function/method.

getPrecondition() - Method in class wyil.lang.WyilFile.FunctionOrMethodOrProperty

Get the list of expressions that make up the precondition of this function/method.

getReadableElementType() - Method in interface wyil.lang.Type.EffectiveArray

Get the element type which could be read from this array.

getReadableElementType() - Method in interface wyil.lang.Type.EffectiveReference

Get the element type which could be read from this array.

getReadableFieldType(String) - Method in interface wyil.lang.Type.EffectiveRecord

Get the element type which could be read from this array.

getSourceFile(Path.ID) - Method in class wyc.builder.CompileTask

Get the source file associated with a given module identifier.

getTree() - Method in class wyil.lang.WyilFile.Declaration

getType() - Method in class wyil.lang.SyntaxTree.Location

Get the declared type of this location.

getType(int) - Method in class wyil.lang.SyntaxTree.Location

Get a specific type of this location.

getTypes() - Method in class wyil.lang.SyntaxTree.Location

Get the types for this location.

getTypeSystem() - Method in class wyc.builder.CompileTask

Access the type system object this compile task is using.

getTypeSystem() - Method in class wyil.util.interpreter.Interpreter

getVariableDeclaration(SyntaxTree.Location<?>) - Method in class wyil.builders.VerificationConditionGenerator

getVariableDeclaration(SyntaxTree.Location<?>) - Method in class wyil.util.interpreter.Interpreter

getVerificationConditions() - Method in class wyc.commands.Compile

getVerify() - Method in class wyc.commands.Compile

getWriteableElementType() - Method in interface wyil.lang.Type.EffectiveArray

Get the element type which could be written to this array.

getWriteableElementType() - Method in interface wyil.lang.Type.EffectiveReference

Get the element type which could be written to this array.

getWriteableFieldType(String) - Method in interface wyil.lang.Type.EffectiveRecord

Get the element type which could be written to this array.

H

hasFalseBranch() - Method in class wyil.lang.Bytecode.If

Check whether this bytecode has a false branch of not.

hasField(String) - Method in interface wyil.lang.Type.EffectiveRecord

Check whether a given field is present in this effective record or not.

hashCode() - Method in class wyautl_old.lang.Automaton

Determine the hashCode of a type.

hashCode() - Method in class wyautl_old.lang.Automaton.State

hashCode() - Method in class wyil.lang.Bytecode.Case

hashCode() - Method in class wyil.lang.Bytecode.Const

hashCode() - Method in class wyil.lang.Bytecode.FieldLoad

hashCode() - Method in class wyil.lang.Bytecode.Index

hashCode() - Method in class wyil.lang.Bytecode.IndirectInvoke

hashCode() - Method in class wyil.lang.Bytecode.Invoke

hashCode() - Method in class wyil.lang.Bytecode.Lambda

hashCode() - Method in class wyil.lang.Bytecode.NamedBlock

hashCode() - Method in class wyil.lang.Bytecode.Range

hashCode() - Method in class wyil.lang.Bytecode.Switch

hashCode() - Method in class wyil.lang.Bytecode.VariableDeclaration

hashCode() - Method in class wyil.lang.Constant.Array

hashCode() - Method in class wyil.lang.Constant.Bool

hashCode() - Method in class wyil.lang.Constant.Byte

hashCode() - Method in class wyil.lang.Constant.FunctionOrMethod

hashCode() - Method in class wyil.lang.Constant.Integer

hashCode() - Method in class wyil.lang.Constant.Null

hashCode() - Method in class wyil.lang.Constant.Record

hashCode() - Method in class wyil.lang.Constant.Type

hashCode() - Method in class wyil.lang.Type.Impl.FunctionOrMethod

hashCode() - Method in class wyil.lang.Type.Impl.Method

hashCode() - Method in class wyil.lang.Type.Impl.Primitive

hashCode() - Method in class wyil.util.AbstractBytecode

hashCode() - Method in class wyil.util.interpreter.Interpreter.ConstantLambda

hashCode() - Method in class wyil.util.interpreter.Interpreter.ConstantObject

hashCode() - Method in class wyil.util.TypeSystem.FunctionOrMethodState

hasModifier(NameID, WhileyFile.Context, Modifier) - Method in class wyc.builder.CompileTask

Determine whether a named item has a modifier matching one of a given list.

hasModifier(Modifier) - Method in class wyc.lang.WhileyFile.NamedDeclaration

hasModifier(Modifier) - Method in class wyil.lang.WyilFile.Declaration

hasName(String) - Method in class wyc.lang.WhileyFile

hasName(String) - Method in class wyil.lang.WyilFile

Determines whether a declaration exists with the given name.

I

id() - Method in class wyc.builder.CompileTask

id() - Method in class wyil.builders.Wyil2WyalBuilder

If(int, int) - Constructor for class wyil.lang.Bytecode.If

If(int, int, int) - Constructor for class wyil.lang.Bytecode.If

IfElse(Expr, List<Stmt>, List<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.IfElse

Construct an if-else statement from a condition, true branch and optional false branch.

IfElse(Expr, List<Stmt>, List<Stmt>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.IfElse

Construct an if-else statement from a condition, true branch and optional false branch.

Impl() - Constructor for class wyil.lang.Type.Impl

Import(Trie, String, Attribute...) - Constructor for class wyc.lang.WhileyFile.Import

imports(Trie) - Method in class wyc.builder.CompileTask

This method takes a given import declaration, and expands it to find all matching modules.

imports() - Method in interface wyc.lang.WhileyFile.Context

INCOMPARABLE_OPERANDS - Static variable in class wyil.util.ErrorMessages

indent(int) - Method in class wyc.io.WhileyFilePrinter

index - Variable in class wyc.lang.Expr.IndexOf

Index(int, int) - Constructor for class wyil.lang.Bytecode.Index

IndexOf(Expr, Expr, Attribute...) - Constructor for class wyc.lang.Expr.IndexOf

IndexOf(Expr, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Expr.IndexOf

IndirectFunctionCall(Expr, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.IndirectFunctionCall

IndirectFunctionCall(Expr, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.IndirectFunctionCall

IndirectFunctionOrMethodCall(Expr, Collection<Expr>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.IndirectFunctionOrMethodCall

IndirectFunctionOrMethodCall(Expr, Collection<Expr>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.IndirectFunctionOrMethodCall

IndirectInvoke(Type.FunctionOrMethod, int, int[]) - Constructor for class wyil.lang.Bytecode.IndirectInvoke

Construct an indirect invocation bytecode which assigns to an optional target register the result from indirectly invoking a function in a given operand with a given set of parameter operands.

IndirectMethodCall(Expr, Collection<Expr>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.IndirectMethodCall

IndirectMethodCall(Expr, Collection<Expr>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.IndirectMethodCall

initialiseProject() - Method in class wyc.util.AbstractProjectCommand

Construct a new temporary project.

Integer(BigInteger) - Constructor for class wyil.lang.Constant.Integer

internalFailure(String, WhileyFile.Context, SyntacticElement) - Static method in class wyc.lang.WhileyFile

internalFailure(String, WhileyFile.Context, SyntacticElement, Throwable) - Static method in class wyc.lang.WhileyFile

Interpreter - Class in wyil.util.interpreter

A simple interpreter for WyIL bytecodes.

Interpreter(Build.Project, PrintStream) - Constructor for class wyil.util.interpreter.Interpreter

Interpreter.ConstantLambda - Class in wyil.util.interpreter

Represents an object allocated on the heap.

Interpreter.ConstantObject - Class in wyil.util.interpreter

Represents an object allocated on the heap.

Interpreter.InternalFunction - Interface in wyil.util.interpreter

An internal function is simply a named internal function.

intersectClosedClosedRecord(Type.Impl.Record, Type.Impl.Record) - Static method in class wyil.lang.Type.Impl

When intersecting two closed records, we require they both have the same set of fields.

Intersection(Type...) - Static method in interface wyil.lang.Type

Construct the intersection of one or more types together.

intersectOpenClosedRecord(Type.Impl.Record, Type.Impl.Record) - Static method in class wyil.lang.Type.Impl

When intersecting an open record with a closed record.

intersectOpenOpenRecord(Type.Impl.Record, Type.Impl.Record) - Static method in class wyil.lang.Type.Impl

When intersecting an open record with another open record, there is always a resulting intersection.

intersectRecords(int, boolean, int, boolean) - Method in class wyil.util.type.ExplicitCoercionOperator

Check for intersection between two states with kind K_RECORD.

intersectRecords(int, boolean, int, boolean) - Method in class wyil.util.type.SubtypeOperator

Check for intersection between two states with kind K_RECORD.

INVALID_ARRAY_EXPRESSION - Static variable in class wyil.util.ErrorMessages

INVALID_BINARY_EXPRESSION - Static variable in class wyil.util.ErrorMessages

INVALID_BOOLEAN_EXPRESSION - Static variable in class wyil.util.ErrorMessages

INVALID_CONSTANT_EXPRESSION - Static variable in class wyil.util.ErrorMessages

INVALID_FILE_ACCESS - Static variable in class wyil.util.ErrorMessages

INVALID_LVAL_EXPRESSION - Static variable in class wyil.util.ErrorMessages

INVALID_NUMERIC_EXPRESSION - Static variable in class wyil.util.ErrorMessages

INVALID_PACKAGE_ACCESS - Static variable in class wyil.util.ErrorMessages

INVALID_TUPLE_LVAL - Static variable in class wyil.util.ErrorMessages

INVALID_UNARY_EXPRESSION - Static variable in class wyil.util.ErrorMessages

invariant - Variable in class wyc.lang.WhileyFile.Type

invariants - Variable in class wyc.lang.Stmt.DoWhile

invariants - Variable in class wyc.lang.Stmt.While

invariants() - Method in class wyil.lang.Bytecode.Loop

Return the array of operands making up the loop invariant.

invertCondition(WyalFile.Expr, SyntaxTree.Location<?>) - Method in class wyil.builders.VerificationConditionGenerator

Generate the logically inverted expression corresponding to a given comparator.

invertConditions(WyalFile.Expr[], SyntaxTree.Location<?>) - Method in class wyil.builders.VerificationConditionGenerator

Invoke(Type.FunctionOrMethod, int[], NameID) - Constructor for class wyil.lang.Bytecode.Invoke

isConcrete(Automaton) - Static method in class wyautl_old.lang.Automata

Check whether or not an automaton is "concrete".

isContractive(Automaton) - Static method in class wyil.util.type.TypeAlgorithms

Contractive types are types which cannot accept value because they have an unterminated cycle.

isContractive(Type) - Method in class wyil.util.TypeSystem

Contractive types are types which cannot accept value because they have an unterminated cycle.

isDefault() - Method in class wyil.lang.Bytecode.Case

isEmpty(Type) - Method in class wyil.util.TypeSystem

Determine whether or not this type corresponds to the empty type or not.

isExplicitCoerciveSubtype(Type, Type, LifetimeRelation) - Method in class wyil.util.TypeSystem

Determine whether type t2 is an explicit coercive subtype of type t1.

isExplicitCoerciveSubtype(Type, Type) - Method in class wyil.util.TypeSystem

Determine whether type t2 is an explicit coercive subtype of type t1.

isFunction() - Method in class wyil.lang.WyilFile.FunctionOrMethodOrProperty

Check whether this represents a function declaration or not.

isIntersection(int, boolean, int, boolean) - Method in class wyil.util.type.SubtypeOperator

Determine whether there is a non-empty intersection between the state rooted at fromIndex and that rooted at toIndex.

isIntersectionInner(int, boolean, int, boolean) - Method in class wyil.util.type.ExplicitCoercionOperator

isIntersectionInner(int, boolean, int, boolean) - Method in class wyil.util.type.SubtypeOperator

isMemberOfType(Constant, Type, SyntacticElement) - Method in class wyil.util.interpreter.Interpreter

Determine whether a given value is a member of a given type.

isMethod() - Method in class wyil.lang.WyilFile.FunctionOrMethodOrProperty

Check whether this represents a method declaration or not.

isName(NameID) - Method in class wyc.builder.CompileTask

Determine whether a given name exists or not.

isNameVisible(NameID, WhileyFile.Context) - Method in class wyc.builder.CompileTask

Determine whether a name is visible in a given context.

isOpen() - Method in interface wyil.lang.Type.Record

Check whether this is an open record or not.

isOpen - Variable in class wyil.util.TypeSystem.RecordState

isOperatorStart(char) - Method in class wyc.io.WhileyFileLexer

isPure(Expr, WhileyFile.Context) - Static method in class wyc.lang.Exprs

Determine whether this expression is "pure" or not.

isSubtype(int, int) - Method in class wyil.util.type.SubtypeOperator

Test whether from :> to

isSubtype(Type, Type, LifetimeRelation) - Method in class wyil.util.TypeSystem

Determine whether type t2 is a subtype of type t1 (written t1 :> t2).

isSubtype(Type, Type) - Method in class wyil.util.TypeSystem

Determine whether type t2 is a subtype of type t1 (written t1 :> t2).

isSupertype(int, int) - Method in class wyil.util.type.SubtypeOperator

Test whether from <: to

isTypeVisible(NameID, WhileyFile.Context) - Method in class wyc.builder.CompileTask

Determine whether a named type is fully visible in a given context.

K

K_ANY - Static variable in class wyil.util.TypeSystem

K_ARRAY - Static variable in class wyil.util.TypeSystem

K_BOOL - Static variable in class wyil.util.TypeSystem

K_BYTE - Static variable in class wyil.util.TypeSystem

K_FUNCTION - Static variable in class wyil.util.TypeSystem

K_INT - Static variable in class wyil.util.TypeSystem

K_INTERSECTION - Static variable in class wyil.util.TypeSystem

K_META - Static variable in class wyil.util.TypeSystem

K_METHOD - Static variable in class wyil.util.TypeSystem

K_NEGATION - Static variable in class wyil.util.TypeSystem

K_NOMINAL - Static variable in class wyil.util.TypeSystem

K_NULL - Static variable in class wyil.util.TypeSystem

K_PROPERTY - Static variable in class wyil.util.TypeSystem

K_RECORD - Static variable in class wyil.util.TypeSystem

K_REFERENCE - Static variable in class wyil.util.TypeSystem

K_UNION - Static variable in class wyil.util.TypeSystem

K_VOID - Static variable in class wyil.util.TypeSystem

keywords - Static variable in class wyc.io.WhileyFileLexer

A map from identifier strings to the corresponding token kind.

kind - Variable in class wyautl_old.lang.Automaton.State

kind - Variable in class wyc.io.WhileyFileLexer.Token

kind() - Method in class wyil.lang.Bytecode.Operator

kind() - Method in class wyil.lang.Bytecode.Quantifier

L

Lambda(Collection<WhileyFile.Parameter>, Collection<String>, Collection<String>, Expr, Attribute...) - Constructor for class wyc.lang.Expr.Lambda

Lambda(Collection<WhileyFile.Parameter>, Collection<String>, Collection<String>, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Expr.Lambda

Lambda(Type.FunctionOrMethod, int, int[], int[]) - Constructor for class wyil.lang.Bytecode.Lambda

Create a new lambda bytecode

leftHandSide() - Method in class wyil.lang.Bytecode.Assign

Returns operand(s) from which assigned value is written to.

LEFTHANDSIDE - Static variable in class wyil.lang.SyntaxTree

lhs - Variable in class wyc.lang.Expr.BinOp

lifetime - Variable in class wyc.lang.Expr.New

lifetime() - Method in interface wyil.lang.Type.Reference

Return the lifetime of this reference.

lifetimeArguments - Variable in class wyc.lang.Expr.AbstractIndirectInvoke

lifetimeArguments - Variable in class wyc.lang.Expr.AbstractInvoke

lifetimeParameters - Variable in class wyc.lang.Expr.AbstractFunctionOrMethod

lifetimeParameters - Variable in class wyc.lang.Expr.Lambda

lifetimeParameters - Variable in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

lifetimeParameters - Variable in class wyil.lang.Type.Impl.Method

lifetimeParameters - Variable in class wyil.util.TypeSystem.FunctionOrMethodState

lifetimeParams() - Method in class wyil.lang.Type.Impl.Method

Get the lifetime parameters of this function or method type.

lifetimeParams() - Method in interface wyil.lang.Type.Method

Get the lifetime parameters declared by this method.

LifetimeRelation - Class in wyil.util.type

This relation tracks the partial order among lifetimes.

LifetimeRelation() - Constructor for class wyil.util.type.LifetimeRelation

Create a new and empty lifetime relation.

LifetimeRelation(LifetimeRelation) - Constructor for class wyil.util.type.LifetimeRelation

Create an independent copy of the given lifetime relation.

LocalVariable(String, Attribute...) - Constructor for class wyc.lang.Expr.LocalVariable

LocalVariable(String, Collection<Attribute>) - Constructor for class wyc.lang.Expr.LocalVariable

Location(SyntaxTree, T, Attribute...) - Constructor for class wyil.lang.SyntaxTree.Location

Location(SyntaxTree, T, List<Attribute>) - Constructor for class wyil.lang.SyntaxTree.Location

Location(SyntaxTree, Type, T, Attribute...) - Constructor for class wyil.lang.SyntaxTree.Location

Location(SyntaxTree, Type, T, List<Attribute>) - Constructor for class wyil.lang.SyntaxTree.Location

Location(SyntaxTree, Type[], T, Attribute...) - Constructor for class wyil.lang.SyntaxTree.Location

Location(SyntaxTree, Type[], T, List<Attribute>) - Constructor for class wyil.lang.SyntaxTree.Location

logger - Variable in class wyc.util.AbstractProjectCommand

The logger used for logging system events

logger - Variable in class wyil.builders.Wyil2WyalBuilder

For logging information.

lookupFunctionOrMethodOrProperty(NameID, Type.FunctionOrMethod, SyntaxTree.Location<?>) - Method in class wyil.builders.VerificationConditionGenerator

Lookup a given function or method.

Loop(int, int, int[], int[]) - Constructor for class wyil.lang.Bytecode.Loop

lvals - Variable in class wyc.lang.Stmt.Assign

M

Method(List<Modifier>, String, List<WhileyFile.Parameter>, List<WhileyFile.Parameter>, List<String>, List<Expr>, List<Expr>, List<Stmt>, Attribute...) - Constructor for class wyc.lang.WhileyFile.Method

Method(Type.Impl[], Type.Impl[]) - Constructor for class wyil.lang.Type.Impl.Method

Method(String[], String[], Type.Impl[], Type.Impl[]) - Constructor for class wyil.lang.Type.Impl.Method

Method(Collection<String>, Collection<String>, Type.Impl[], Type.Impl[]) - Constructor for class wyil.lang.Type.Impl.Method

Method(Type[], Type[]) - Static method in interface wyil.lang.Type

Method(Collection<String>, Collection<String>, Type[], Type[]) - Static method in interface wyil.lang.Type

Method(String[], String[], Type[], Type[]) - Static method in interface wyil.lang.Type

MethodCall(NameID, Path.ID, Collection<Expr>, Collection<String>, Attribute...) - Constructor for class wyc.lang.Expr.MethodCall

MethodCall(NameID, Path.ID, Collection<Expr>, Collection<String>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.MethodCall

METHODCALL_NOT_PERMITTED - Static variable in class wyil.util.ErrorMessages

methodType - Variable in class wyc.lang.Expr.IndirectMethodCall

methodType - Variable in class wyc.lang.Expr.MethodCall

mhs - Variable in class wyc.lang.Expr.UnOp

minimise(Automaton) - Static method in class wyautl_old.lang.Automata

This method minimises an automaton by removing equivalent states.

MISSING_RETURN_VALUE - Static variable in class wyil.util.ErrorMessages

modifiedVariables() - Method in class wyil.lang.Bytecode.Loop

Return the array of modified variables which are those assigned (in some way) in the body of the loop.

Modifier - Interface in wyil.lang

Represents a protection modifier on a module item.

Modifier.Export - Class in wyil.lang

Modifier.Native - Class in wyil.lang

Modifier.Private - Class in wyil.lang

Modifier.Public - Class in wyil.lang

MODIFIER_Export - Static variable in class wyil.io.WyilFileWriter

MODIFIER_MANGLE_MASK - Static variable in class wyil.io.WyilFileWriter

MODIFIER_Native - Static variable in class wyil.io.WyilFileWriter

MODIFIER_Private - Static variable in class wyil.io.WyilFileWriter

MODIFIER_PROTECTION_MASK - Static variable in class wyil.io.WyilFileWriter

MODIFIER_Public - Static variable in class wyil.io.WyilFileWriter

modifiers() - Method in class wyc.lang.WhileyFile.NamedDeclaration

modifiers() - Method in class wyil.lang.WyilFile.Declaration

ModuleCheck - Class in wyc.builder

Performs a number of simplistic checks that a module is syntactically correct.

ModuleCheck(WhileyFile) - Constructor for class wyc.builder.ModuleCheck

ModuleReader - Interface in wyil.io

A module reader is responsible for physically reading information about a given module.

MoveAnalysis - Class in wyil.util

Responsible for determining when a value of a dynamically sized data type can be "moved" or must be "copied".

MoveAnalysis(Build.Task) - Constructor for class wyil.util.MoveAnalysis

mustParseAsMixedType() - Method in class wyc.io.WhileyFileParser

N

name - Variable in class wyc.lang.Expr.AbstractFunctionOrMethod

name - Variable in class wyc.lang.Expr.AbstractInvoke

name - Variable in class wyc.lang.Expr.ConstantAccess

name - Variable in class wyc.lang.Expr.FieldAccess

name - Variable in class wyc.lang.Expr.Record

name - Variable in class wyc.lang.Stmt.NamedBlock

name - Variable in class wyc.lang.WhileyFile.Import

name() - Method in class wyc.lang.WhileyFile.NamedDeclaration

name - Variable in class wyc.lang.WhileyFile.Parameter

name() - Method in class wyc.lang.WhileyFile.Parameter

name() - Method in class wyil.lang.Bytecode.Invoke

name() - Method in class wyil.lang.Constant.FunctionOrMethod

name() - Method in interface wyil.lang.Type.Nominal

name() - Method in class wyil.lang.WyilFile.Declaration

NamedBlock(String, Collection<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.NamedBlock

Construct a named block from a given name and body of statements.

NamedBlock(String, Collection<Stmt>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.NamedBlock

Construct a named block from a given name and body of statements.

NamedBlock(int, String) - Constructor for class wyil.lang.Bytecode.NamedBlock

NamedDeclaration(String, Collection<Modifier>, Attribute...) - Constructor for class wyc.lang.WhileyFile.NamedDeclaration

NARY_ASSIGNABLE - Static variable in interface wyil.lang.Bytecode

NATIVE - Static variable in interface wyil.lang.Modifier

Negation(Type) - Static method in interface wyil.lang.Type

Construct the negation of a given type.

New(Expr, String, Attribute...) - Constructor for class wyc.lang.Expr.New

next() - Method in class wyil.lang.Bytecode.Index

next(int) - Method in class wyil.lang.Bytecode.Index

nid - Variable in class wyc.lang.Expr.FunctionOrMethod

nid - Variable in class wyc.lang.Expr.FunctionOrMethodCall

nid() - Method in class wyc.lang.Expr.FunctionOrMethodCall

NOCHILDREN - Static variable in class wyautl_old.lang.Automaton

The following constant is used simply to prevent unnecessary memory allocations.

Nominal(NameID) - Static method in interface wyil.lang.Type

Null - Static variable in class wyil.lang.Constant

The Null constant value

Null() - Constructor for class wyil.lang.Constant.Null

numberOfBlocks() - Method in interface wyil.lang.Bytecode.Stmt

Determine the number of blocks contained in this bytecode.

numberOfBlocks() - Method in class wyil.lang.SyntaxTree.Location

Get the number of blocks contained in this statement.

numberOfBlocks() - Method in class wyil.util.AbstractBytecode

Determine the number of blocks contained in this bytecode.

numberOfOperandGroups() - Method in interface wyil.lang.Bytecode

Get the number of operand groups in this bytecode

numberOfOperandGroups() - Method in class wyil.lang.SyntaxTree.Location

Get the number of operand groups in this location.

numberOfOperandGroups() - Method in class wyil.util.AbstractBytecode

Get the number of operand groups in this bytecode

numberOfOperands() - Method in interface wyil.lang.Bytecode

Get the number of operands in this bytecode

numberOfOperands() - Method in class wyil.lang.SyntaxTree.Location

Get the number of operand groups in this location.

numberOfOperands() - Method in class wyil.util.AbstractBytecode

Return the number of top-level operands in this bytecode

numberOfTypes() - Method in class wyil.lang.SyntaxTree.Location

Get the number of types declared by this location.

numParams - Variable in class wyil.util.TypeSystem.FunctionOrMethodState

O

offset() - Method in class wyil.lang.Bytecode.Index

op - Variable in class wyc.lang.Expr.BinOp

op - Variable in class wyc.lang.Expr.UnOp

opcode - Variable in enum wyil.lang.Bytecode.OperatorKind

opcode - Variable in enum wyil.lang.Bytecode.QuantifierKind

OPCODE_add - Static variable in interface wyil.lang.Bytecode

OPCODE_aliasdecl - Static variable in interface wyil.lang.Bytecode

OPCODE_all - Static variable in interface wyil.lang.Bytecode

OPCODE_array - Static variable in interface wyil.lang.Bytecode

OPCODE_arraygen - Static variable in interface wyil.lang.Bytecode

OPCODE_arrayindex - Static variable in interface wyil.lang.Bytecode

OPCODE_arraylength - Static variable in interface wyil.lang.Bytecode

OPCODE_assert - Static variable in interface wyil.lang.Bytecode

OPCODE_assign - Static variable in interface wyil.lang.Bytecode

OPCODE_assume - Static variable in interface wyil.lang.Bytecode

OPCODE_bitwiseand - Static variable in interface wyil.lang.Bytecode

OPCODE_bitwiseinvert - Static variable in interface wyil.lang.Bytecode

OPCODE_bitwiseor - Static variable in interface wyil.lang.Bytecode

OPCODE_bitwisexor - Static variable in interface wyil.lang.Bytecode

OPCODE_block - Static variable in interface wyil.lang.Bytecode

OPCODE_break - Static variable in interface wyil.lang.Bytecode

OPCODE_const - Static variable in interface wyil.lang.Bytecode

OPCODE_continue - Static variable in interface wyil.lang.Bytecode

OPCODE_convert - Static variable in interface wyil.lang.Bytecode

OPCODE_debug - Static variable in interface wyil.lang.Bytecode

OPCODE_dereference - Static variable in interface wyil.lang.Bytecode

OPCODE_div - Static variable in interface wyil.lang.Bytecode

OPCODE_dowhile - Static variable in interface wyil.lang.Bytecode

OPCODE_eq - Static variable in interface wyil.lang.Bytecode

OPCODE_fail - Static variable in interface wyil.lang.Bytecode

OPCODE_fieldload - Static variable in interface wyil.lang.Bytecode

OPCODE_ge - Static variable in interface wyil.lang.Bytecode

OPCODE_gt - Static variable in interface wyil.lang.Bytecode

OPCODE_if - Static variable in interface wyil.lang.Bytecode

OPCODE_ifelse - Static variable in interface wyil.lang.Bytecode

OPCODE_ifis - Static variable in interface wyil.lang.Bytecode

OPCODE_indirectinvoke - Static variable in interface wyil.lang.Bytecode

OPCODE_invoke - Static variable in interface wyil.lang.Bytecode

OPCODE_is - Static variable in interface wyil.lang.Bytecode

OPCODE_lambda - Static variable in interface wyil.lang.Bytecode

OPCODE_le - Static variable in interface wyil.lang.Bytecode

OPCODE_logicaland - Static variable in interface wyil.lang.Bytecode

OPCODE_logicalnot - Static variable in interface wyil.lang.Bytecode

OPCODE_logicalor - Static variable in interface wyil.lang.Bytecode

OPCODE_lt - Static variable in interface wyil.lang.Bytecode

OPCODE_mul - Static variable in interface wyil.lang.Bytecode

OPCODE_namedblock - Static variable in interface wyil.lang.Bytecode

OPCODE_ne - Static variable in interface wyil.lang.Bytecode

OPCODE_neg - Static variable in interface wyil.lang.Bytecode

OPCODE_newobject - Static variable in interface wyil.lang.Bytecode

OPCODE_record - Static variable in interface wyil.lang.Bytecode

OPCODE_rem - Static variable in interface wyil.lang.Bytecode

OPCODE_return - Static variable in interface wyil.lang.Bytecode

OPCODE_shl - Static variable in interface wyil.lang.Bytecode

OPCODE_shr - Static variable in interface wyil.lang.Bytecode

OPCODE_skip - Static variable in interface wyil.lang.Bytecode

OPCODE_some - Static variable in interface wyil.lang.Bytecode

OPCODE_sub - Static variable in interface wyil.lang.Bytecode

OPCODE_switch - Static variable in interface wyil.lang.Bytecode

OPCODE_varcopy - Static variable in interface wyil.lang.Bytecode

OPCODE_vardecl - Static variable in interface wyil.lang.Bytecode

OPCODE_vardeclinit - Static variable in interface wyil.lang.Bytecode

OPCODE_varmove - Static variable in interface wyil.lang.Bytecode

OPCODE_while - Static variable in interface wyil.lang.Bytecode

operand() - Method in class wyil.lang.Bytecode.AssertOrAssume

operand() - Method in class wyil.lang.Bytecode.Convert

operand() - Method in class wyil.lang.Bytecode.FieldLoad

operand() - Method in class wyil.lang.Bytecode.Switch

Operator(int[], Bytecode.OperatorKind) - Constructor for class wyil.lang.Bytecode.Operator

outlives(String, String) - Method in class wyil.util.type.LifetimeRelation

Check whether the first (outer) lifetime outlives the second (inner) lifetime.

P

parameter - Variable in class wyc.lang.Stmt.VariableDeclaration

Parameter(WyalFile.Type, String, Attribute...) - Constructor for class wyc.lang.WhileyFile.Parameter

Parameter(WyalFile.Type, String, Collection<Attribute>) - Constructor for class wyc.lang.WhileyFile.Parameter

parameter - Variable in class wyc.lang.WhileyFile.Type

parameter(int) - Method in interface wyil.lang.Type.FunctionOrMethod

Get the ith parameter type

parameter(int) - Method in class wyil.lang.Type.Impl.FunctionOrMethod

parameters - Variable in class wyc.lang.Expr.Lambda

parameters - Variable in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

parameters() - Method in class wyil.lang.Bytecode.Lambda

PARAMETERS - Static variable in class wyil.lang.SyntaxTree

parameters - Variable in class wyil.lang.Type.Impl.FunctionOrMethod

params() - Method in interface wyil.lang.Type.FunctionOrMethod

Get the list of parameter types which are accepted by this function or method.

params() - Method in class wyil.lang.Type.Impl.FunctionOrMethod

Get the parameter types of this function or method type.

paramTypes - Variable in class wyc.lang.Expr.AbstractFunctionOrMethod

parent() - Method in class wyil.lang.WyilFile.Block

Get the WyIL file enclosing this block

parse() - Method in class wyil.util.type.TypeParser

parse(HashSet<String>) - Method in class wyil.util.type.TypeParser

parseBraceTerm(HashSet<String>) - Method in class wyil.util.type.TypeParser

parseDefiniteType(WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

Attempt to parse something which maybe a type, or an expression.

parseExpressions(WhileyFile, WhileyFileParser.EnclosingScope, boolean) - Method in class wyc.io.WhileyFileParser

Parse a "multi-expression"; that is, a sequence of one or more expressions separated by comma's

parseNotTerm(HashSet<String>) - Method in class wyil.util.type.TypeParser

parseOptionalContextLifetimes(WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

parseOptionalLifetimeParameters(WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

Attention: Enters the lifetime names to the passed scope!

parseOptionalParameter(WhileyFile, WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

parseOptionalParameters(WhileyFile, WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

parseOptionalParameterTypes(WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

parseParameters(WhileyFile, WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

parseParameterTypes(WhileyFileParser.EnclosingScope) - Method in class wyc.io.WhileyFileParser

parseString(String) - Method in class wyc.io.WhileyFileParser

Parse a string constant whilst interpreting all escape characters.

parseTerm(HashSet<String>) - Method in class wyil.util.type.TypeParser

parseTypeDeclaration(WhileyFile, List<Modifier>) - Method in class wyc.io.WhileyFileParser

Parse a type declaration in a Whiley source file, which has the form:

PositiveAtom() - Constructor for class wyil.lang.Type.Impl.PositiveAtom

print(WhileyFile) - Method in class wyc.io.WhileyFilePrinter

print(WhileyFile.Declaration) - Method in class wyc.io.WhileyFilePrinter

print(WhileyFile.FunctionOrMethodOrProperty) - Method in class wyc.io.WhileyFilePrinter

print(WhileyFile.Import) - Method in class wyc.io.WhileyFilePrinter

print(WhileyFile.Constant) - Method in class wyc.io.WhileyFilePrinter

print(WhileyFile.Type) - Method in class wyc.io.WhileyFilePrinter

print(List<Stmt>, int) - Method in class wyc.io.WhileyFilePrinter

print(Stmt, int) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Assert) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Assume) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Debug) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Break) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Continue) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Skip) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Return) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Assign) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.IfElse, int) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.DoWhile, int) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.NamedBlock, int) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.While, int) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.Switch, int) - Method in class wyc.io.WhileyFilePrinter

print(Stmt.VariableDeclaration, int) - Method in class wyc.io.WhileyFilePrinter

print(Expr) - Method in class wyc.io.WhileyFilePrinter

print(Expr.Constant) - Method in class wyc.io.WhileyFilePrinter

print(Expr.AbstractVariable) - Method in class wyc.io.WhileyFilePrinter

print(Expr.ConstantAccess) - Method in class wyc.io.WhileyFilePrinter

print(Expr.ArrayInitialiser) - Method in class wyc.io.WhileyFilePrinter

print(Expr.BinOp) - Method in class wyc.io.WhileyFilePrinter

print(Expr.Dereference) - Method in class wyc.io.WhileyFilePrinter

print(Expr.Cast) - Method in class wyc.io.WhileyFilePrinter

print(Expr.IndexOf) - Method in class wyc.io.WhileyFilePrinter

print(Expr.UnOp) - Method in class wyc.io.WhileyFilePrinter

print(Expr.AbstractInvoke) - Method in class wyc.io.WhileyFilePrinter

print(Expr.IndirectFunctionCall) - Method in class wyc.io.WhileyFilePrinter

print(Expr.IndirectMethodCall) - Method in class wyc.io.WhileyFilePrinter

print(Expr.Quantifier) - Method in class wyc.io.WhileyFilePrinter

print(Expr.FieldAccess) - Method in class wyc.io.WhileyFilePrinter

print(Expr.Record) - Method in class wyc.io.WhileyFilePrinter

print(Expr.AbstractFunctionOrMethod) - Method in class wyc.io.WhileyFilePrinter

print(Expr.Lambda) - Method in class wyc.io.WhileyFilePrinter

print(Expr.New) - Method in class wyc.io.WhileyFilePrinter

print(Expr.TypeVal) - Method in class wyc.io.WhileyFilePrinter

print(List<Modifier>) - Method in class wyc.io.WhileyFilePrinter

print(WyalFile.Type) - Method in class wyc.io.WhileyFilePrinter

printWithBrackets(Expr, Class<? extends Expr>...) - Method in class wyc.io.WhileyFilePrinter

PRIVATE - Static variable in interface wyil.lang.Modifier

project() - Method in class wyc.builder.CompileTask

project() - Method in class wyc.builder.DecompileTask

project - Variable in class wyil.builders.Wyil2WyalBuilder

The master namespace for identifying all resources available to the builder.

project() - Method in class wyil.builders.Wyil2WyalBuilder

proof - Variable in class wyc.commands.Compile

Signals the proof should be printed during verification.

propagate(List<WhileyFile>) - Method in class wyc.builder.FlowTypeChecker

propagate(WhileyFile) - Method in class wyc.builder.FlowTypeChecker

propagate(WhileyFile.Type) - Method in class wyc.builder.FlowTypeChecker

Resolve types for a given type declaration.

propagate(WhileyFile.Constant) - Method in class wyc.builder.FlowTypeChecker

Propagate and check types for a given constant declaration.

propagate(WhileyFile.FunctionOrMethodOrProperty) - Method in class wyc.builder.FlowTypeChecker

Propagate and check types for a given function or method declaration.

propagate(Expr, FlowTypeChecker.Environment, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

Propagate types through a given expression, whilst checking that it is well typed.

propagateCondition(Expr, boolean, FlowTypeChecker.Environment, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

Propagate type information through an expression being used as a condition, whilst checking it is well-typed at the same time.

Property(List<Modifier>, String, List<WhileyFile.Parameter>, List<Expr>, Attribute...) - Constructor for class wyc.lang.WhileyFile.Property

Property(Type.Impl[]) - Constructor for class wyil.lang.Type.Impl.Property

Property(Type[]) - Static method in interface wyil.lang.Type

Property(WyilFile, Collection<Modifier>, String, Type.Property, Attribute...) - Constructor for class wyil.lang.WyilFile.Property

PropertyCall(NameID, Path.ID, Collection<Expr>, Attribute...) - Constructor for class wyc.lang.Expr.PropertyCall

PropertyCall(NameID, Path.ID, Collection<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Expr.PropertyCall

propertyType - Variable in class wyc.lang.Expr.PropertyCall

PUBLIC - Static variable in interface wyil.lang.Modifier

Q

qualification - Variable in class wyc.lang.Expr.AbstractInvoke

qualification - Variable in class wyc.lang.Expr.ConstantAccess

Quantifier(Expr.QOp, Collection<Triple<String, Expr, Expr>>, Expr, Attribute...) - Constructor for class wyc.lang.Expr.Quantifier

Quantifier(Bytecode.QuantifierKind, int, Bytecode.Range...) - Constructor for class wyil.lang.Bytecode.Quantifier

R

Range(int, int, int) - Constructor for class wyil.lang.Bytecode.Range

ranges() - Method in class wyil.lang.Bytecode.Quantifier

read() - Method in class wyc.io.WhileyFileParser

Read a WhileyFile from the token stream.

read(Path.ID, InputStream) - Method in interface wyil.io.ModuleReader

Read a given given module from an input stream.

read() - Method in class wyil.io.WyilFileReader

read() - Method in class wyil.util.interpreter.Interpreter.ConstantObject

Record(String, Map<String, Expr>, Attribute...) - Constructor for class wyc.lang.Expr.Record

Record(Map<String, Constant>) - Constructor for class wyil.lang.Constant.Record

Record(boolean, List<Pair<Type, String>>) - Static method in interface wyil.lang.Type

Record(boolean, Pair<Type, String>...) - Static method in interface wyil.lang.Type

RECORD_MISSING_FIELD - Static variable in class wyil.util.ErrorMessages

RECORD_TYPE_REQUIRED - Static variable in class wyil.util.ErrorMessages

RecordState(boolean) - Constructor for class wyil.util.TypeSystem.RecordState

RecordState(boolean, Collection<String>) - Constructor for class wyil.util.TypeSystem.RecordState

reference() - Method in class wyil.lang.Bytecode.IndirectInvoke

Return operand holding the indirect function/method reference.

Reference(String, Type) - Static method in interface wyil.lang.Type

REFERENCE_ACCESS_NOT_PERMITTED - Static variable in class wyil.util.ErrorMessages

REFERENCE_NOT_PERMITTED - Static variable in class wyil.util.ErrorMessages

REFERENCE_TYPE_REQUIRED - Static variable in class wyil.util.ErrorMessages

registry - Variable in class wyc.Activator

The master project content type registry.

Registry() - Constructor for class wyc.Activator.Registry

registry - Variable in class wyc.util.AbstractProjectCommand

The master project content type registry.

remap(Automaton.State, int[]) - Static method in class wyautl_old.lang.Automata

The remap method takes a node, and mapping from vertices in the old space to the those in the new space.

replace(WyilFile.Block, WyilFile.Block) - Method in class wyil.lang.WyilFile

replaceWithMerge(LifetimeRelation, LifetimeRelation) - Method in class wyil.util.type.LifetimeRelation

Replace this lifetime relation with the merge result of the given two relations.

requires - Variable in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

RESOLUTION_ERROR - Static variable in class wyil.util.ErrorMessages

resolveAsConstant(NameID) - Method in class wyc.builder.FlowTypeChecker

Resolve a given name as a constant value.

resolveAsConstant(Expr, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

Resolve a given constant expression as a constant value.

resolveAsFunctionOrMethod(NameID, List<Type>, List<String>, WhileyFile.Context, FlowTypeChecker.Environment) - Method in class wyc.builder.FlowTypeChecker

Responsible for determining the true type of a method or function being invoked.

resolveAsFunctionOrMethod(String, WhileyFile.Context, FlowTypeChecker.Environment) - Method in class wyc.builder.FlowTypeChecker

Responsible for determining the true type of a method or function being invoked.

resolveAsFunctionOrMethod(String, List<Type>, List<String>, WhileyFile.Context, FlowTypeChecker.Environment) - Method in class wyc.builder.FlowTypeChecker

Responsible for determining the true type of a method or function being invoked.

resolveAsModule(String, WhileyFile.Context) - Method in class wyc.builder.CompileTask

This method attempts to resolve a name as a module in a given name context.

resolveAsName(String, WhileyFile.Context) - Method in class wyc.builder.CompileTask

Responsible for resolve names, types, constants and functions / methods at the global level.

resolveAsName(List<String>, WhileyFile.Context) - Method in class wyc.builder.CompileTask

This methods attempts to resolve the given list of names into a single named item (e.g.

resolveAsType(WyalFile.Type.Function, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

resolveAsType(WyalFile.Type.Method, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

resolveAsType(WyalFile.Type.Property, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

resolveAsType(WyalFile.Type.FunctionOrMethodOrProperty, WhileyFile.Context) - Method in class wyc.builder.FlowTypeChecker

resolvedType - Variable in class wyc.lang.WhileyFile.Function

resolvedType() - Method in class wyc.lang.WhileyFile.Function

resolvedType() - Method in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

resolvedType - Variable in class wyc.lang.WhileyFile.Method

resolvedType() - Method in class wyc.lang.WhileyFile.Method

resolvedType - Variable in class wyc.lang.WhileyFile.Property

resolvedType() - Method in class wyc.lang.WhileyFile.Property

resolvedType - Variable in class wyc.lang.WhileyFile.Type

resolvedValue - Variable in class wyc.lang.WhileyFile.Constant

result() - Method in class wyc.lang.Expr.AbstractFunctionOrMethod

result() - Method in class wyc.lang.Expr.AbstractIndirectInvoke

result() - Method in class wyc.lang.Expr.AbstractInvoke

result() - Method in class wyc.lang.Expr.AbstractVariable

result() - Method in class wyc.lang.Expr.ArrayGenerator

result() - Method in class wyc.lang.Expr.ArrayInitialiser

result() - Method in class wyc.lang.Expr.BinOp

result() - Method in class wyc.lang.Expr.Cast

result() - Method in class wyc.lang.Expr.Constant

result() - Method in class wyc.lang.Expr.ConstantAccess

result() - Method in class wyc.lang.Expr.Dereference

result() - Method in class wyc.lang.Expr.FieldAccess

result() - Method in class wyc.lang.Expr.FunctionCall

result() - Method in class wyc.lang.Expr.IndexOf

result() - Method in class wyc.lang.Expr.IndirectFunctionCall

result() - Method in class wyc.lang.Expr.IndirectMethodCall

result() - Method in class wyc.lang.Expr.Lambda

result() - Method in class wyc.lang.Expr.LocalVariable

result() - Method in class wyc.lang.Expr.MethodCall

result() - Method in class wyc.lang.Expr.New

result() - Method in class wyc.lang.Expr.PropertyCall

result() - Method in class wyc.lang.Expr.Quantifier

result() - Method in class wyc.lang.Expr.Record

result() - Method in interface wyc.lang.Expr

Get the type that this expression will evaluate to.

result() - Method in class wyc.lang.Expr.TypeVal

result() - Method in class wyc.lang.Expr.UnOp

Return(List<Expr>, Attribute...) - Constructor for class wyc.lang.Stmt.Return

Create a given return statement with an optional return value.

Return(List<Expr>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Return

Create a given return statement with an optional return value.

Return() - Constructor for class wyil.lang.Bytecode.Return

Return(int...) - Constructor for class wyil.lang.Bytecode.Return

RETURN_FROM_VOID - Static variable in class wyil.util.ErrorMessages

returns() - Method in class wyc.lang.Expr.FunctionOrMethodCall

returns() - Method in class wyc.lang.Expr.IndirectFunctionOrMethodCall

returns() - Method in interface wyc.lang.Expr.Multi

Get all the return types this expression can produce.

returns - Variable in class wyc.lang.Stmt.Return

returns - Variable in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

returns() - Method in interface wyil.lang.Type.FunctionOrMethod

Get the list of types which are returned by this function or method.

returns - Variable in class wyil.lang.Type.Impl.FunctionOrMethod

returns() - Method in class wyil.lang.Type.Impl.FunctionOrMethod

Get the return types of this function or method type.

rhs - Variable in class wyc.lang.Expr.BinOp

rightHandSide() - Method in class wyil.lang.Bytecode.Assign

Returns operand(s) from which assigned value is read.

RIGHTHANDSIDE - Static variable in class wyil.lang.SyntaxTree

Run - Class in wyc.commands

Run(Content.Registry, Logger) - Constructor for class wyc.commands.Run

run() - Method in class wyc.util.TestUtils.StreamGrabber

Run.Result - Enum in wyc.commands

Result kind for this command

rvals - Variable in class wyc.lang.Stmt.Assign

S

scan() - Method in class wyc.io.WhileyFileLexer

Scan all characters from the input stream and generate a corresponding list of tokens, whilst discarding all whitespace and comments.

scanBlockComment() - Method in class wyc.io.WhileyFileLexer

scanCharacterConstant() - Method in class wyc.io.WhileyFileLexer

Scan a character constant, such as e.g.

scanIdentifier() - Method in class wyc.io.WhileyFileLexer

scanIndent() - Method in class wyc.io.WhileyFileLexer

Scan one or more spaces or tab characters, combining them to form an "indent".

scanLineComment() - Method in class wyc.io.WhileyFileLexer

scanNumericConstant() - Method in class wyc.io.WhileyFileLexer

Scan a numeric constant.

scanOperator() - Method in class wyc.io.WhileyFileLexer

scanStringConstant() - Method in class wyc.io.WhileyFileLexer

scanWhiteSpace(List<WhileyFileLexer.Token>) - Method in class wyc.io.WhileyFileLexer

Schema(Bytecode.Operands, Bytecode.Extras...) - Constructor for class wyil.lang.Bytecode.Schema

Schema(Bytecode.Operands, Bytecode.OperandGroups, Bytecode.Extras...) - Constructor for class wyil.lang.Bytecode.Schema

Schema(Bytecode.Operands, Bytecode.OperandGroups, Bytecode.Blocks, Bytecode.Extras...) - Constructor for class wyil.lang.Bytecode.Schema

schemas - Static variable in class wyil.util.AbstractBytecode

================================================================== Individual Bytecode Schemas ==================================================================

set(int, int, boolean) - Method in class wyautl_old.util.BinaryMatrix

set(String, Object) - Method in class wyc.commands.Compile

set(String, Object) - Method in class wyc.util.AbstractProjectCommand

setBody(SyntaxTree.Location<Bytecode.Block>) - Method in class wyil.lang.WyilFile.FunctionOrMethod

setBrief() - Method in class wyc.commands.Compile

setExcludes(Content.Filter<WhileyFile>) - Method in class wyc.commands.Compile

setExcludes(String) - Method in class wyc.util.AntTask

setIncludes(Content.Filter<WhileyFile>) - Method in class wyc.commands.Compile

setIncludes(String) - Method in class wyc.util.AntTask

setLogger(Logger) - Method in class wyc.builder.CompileTask

setLogger(Logger) - Method in class wyil.builders.Wyil2WyalBuilder

setVcg(boolean) - Method in class wyc.util.AntTask

setVerbose() - Method in class wyc.commands.Compile

setVerbose(boolean) - Method in class wyc.commands.Compile

setVerbose() - Method in class wyc.commands.Decompile

setVerbose(boolean) - Method in class wyc.util.AntTask

setVerbose(boolean) - Method in class wyil.io.WyilFilePrinter

setVerificationConditions(boolean) - Method in class wyc.commands.Compile

setVerify(boolean) - Method in class wyc.commands.Compile

setVerify(boolean) - Method in class wyc.util.AntTask

setWhileydir(File) - Method in class wyc.util.AbstractProjectCommand

setWhileydir(File) - Method in class wyc.util.AntTask

setWhileypath(String) - Method in class wyc.util.AbstractProjectCommand

setWhileypath(String) - Method in class wyc.util.AntTask

setWyaldir(File) - Method in class wyc.util.AbstractProjectCommand

setWyaldir(File) - Method in class wyc.util.AntTask

setWyildir(File) - Method in class wyc.util.AbstractProjectCommand

setWyildir(File) - Method in class wyc.util.AntTask

simplify(Automaton) - Static method in class wyil.util.type.TypeAlgorithms

Analyse an automaton and try to produce a version that is simpler but still equivalent.

size() - Method in class wyautl_old.lang.Automaton

size() - Method in class wyil.lang.SyntaxTree

Returns the number of locations in this syntax tree.

size() - Method in interface wyil.lang.Type.EffectiveRecord

Return the number of fields in this type

size() - Method in interface wyil.lang.Type.Record

Get the number of fields in this record

Skip(Attribute...) - Constructor for class wyc.lang.Stmt.Skip

Skip(Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Skip

Skip() - Constructor for class wyil.lang.Bytecode.Skip

skipWhitespace(List<WhileyFileLexer.Token>) - Method in class wyc.io.WhileyFileLexer

Skip over any whitespace at the current index position in the input string.

sources - Variable in class wyc.lang.Expr.Quantifier

src - Variable in class wyc.lang.Expr.AbstractIndirectInvoke

src - Variable in class wyc.lang.Expr.Dereference

src - Variable in class wyc.lang.Expr.FieldAccess

src - Variable in class wyc.lang.Expr.IndexOf

srcType - Variable in class wyc.lang.Expr.BinOp

srcType() - Method in class wyc.lang.Expr.BinOp

srcType - Variable in class wyc.lang.Expr.Dereference

srcType - Variable in class wyc.lang.Expr.FieldAccess

srcType - Variable in class wyc.lang.Expr.IndexOf

StandardFunctions - Class in wyil.util.interpreter

StandardFunctions() - Constructor for class wyil.util.interpreter.StandardFunctions

standardFunctions - Static variable in class wyil.util.interpreter.StandardFunctions

The standard functions for use with the interpreter.

start(Module.Context) - Method in class wyc.Activator

start - Variable in class wyc.io.WhileyFileLexer.Token

START - Static variable in class wyil.lang.SyntaxTree

startNamedBlock(String) - Method in class wyil.util.type.LifetimeRelation

Enter a named block to this relation.

startOperand() - Method in class wyil.lang.Bytecode.Range

Return the start operand of this range.

State(int) - Constructor for class wyautl_old.lang.Automaton.State

Construct a deterministic state with no children and no supplementary data.

State(int, int...) - Constructor for class wyautl_old.lang.Automaton.State

Construct a deterministic state with no supplementary data.

State(int, boolean, int...) - Constructor for class wyautl_old.lang.Automaton.State

Construct a state with no supplementary data.

State(int, Object, boolean, int...) - Constructor for class wyautl_old.lang.Automaton.State

Construct a state with children and supplementary data.

State(Automaton.State) - Constructor for class wyautl_old.lang.Automaton.State

statements - Variable in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

states - Variable in class wyautl_old.lang.Automaton

Stmt - Interface in wyc.lang

Provides classes for representing statements in Whiley's source language.

Stmt.Assert - Class in wyc.lang

Represents a assert statement of the form assert e, where e is a boolean expression.

Stmt.Assign - Class in wyc.lang

Represents an assignment statement of the form lhs = rhs.

Stmt.Assume - Class in wyc.lang

Represents an assume statement of the form assume e, where e is a boolean expression.

Stmt.Break - Class in wyc.lang

Stmt.Case - Class in wyc.lang

Stmt.Continue - Class in wyc.lang

Stmt.Debug - Class in wyc.lang

Stmt.DoWhile - Class in wyc.lang

Represents a do-while statement whose body is made up from a block of statements separated by indentation.

Stmt.Fail - Class in wyc.lang

Represents a fail statement.

Stmt.IfElse - Class in wyc.lang

Represents a classical if-else statement, which is has the form:

Stmt.NamedBlock - Class in wyc.lang

Represents a named block, which has the form:

Stmt.Return - Class in wyc.lang

Represents a return statement, which has the form:

Stmt.Skip - Class in wyc.lang

Stmt.Switch - Class in wyc.lang

Stmt.VariableDeclaration - Class in wyc.lang

Represents a variable declaration which has the form:

Stmt.While - Class in wyc.lang

Represents a while statement, which has the form:

stmts - Variable in class wyc.lang.Stmt.Case

stop(Module, Module.Context) - Method in class wyc.Activator

StreamGrabber(InputStream, StringBuffer) - Constructor for class wyc.util.TestUtils.StreamGrabber

SUBTYPE_ERROR - Static variable in class wyil.util.ErrorMessages

SubtypeOperator - Class in wyil.util.type

The subtype operator implements the algorithm for determining whether or not one type is a subtype of another.

SubtypeOperator(Automaton, Automaton, LifetimeRelation) - Constructor for class wyil.util.type.SubtypeOperator

suffix(Content.Type<?>) - Method in class wyc.Activator.Registry

Switch(Expr, List<Stmt.Case>, Attribute...) - Constructor for class wyc.lang.Stmt.Switch

Switch(Expr, List<Stmt.Case>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.Switch

Switch(int, Bytecode.Case[]) - Constructor for class wyil.lang.Bytecode.Switch

SyntacticType - Interface in wyc.lang

Provides classes for representing types in Whiley's source language.

syntaxError(String, WhileyFile.Context, SyntacticElement) - Static method in class wyc.lang.WhileyFile

syntaxError(String, WhileyFile.Context, SyntacticElement, Throwable) - Static method in class wyc.lang.WhileyFile

SyntaxTree - Class in wyil.lang

A SyntaxTree representation of the Whiley Intermediate Language (WyIL).

SyntaxTree(WyilFile.Declaration) - Constructor for class wyil.lang.SyntaxTree

SyntaxTree.Location<T extends Bytecode> - Class in wyil.lang

SyntaxTrees - Class in wyil.util

Helper functions for working with SyntaxTrees.

SyntaxTrees() - Constructor for class wyil.util.SyntaxTrees

T

T_ANY - Static variable in interface wyil.lang.Type

The type any represents the type whose variables may hold any possible value.

T_BOOL - Static variable in interface wyil.lang.Type

Represents the set of boolean values (i.e.

T_BYTE - Static variable in interface wyil.lang.Type

Represents a sequence of 8 bits.

T_INT - Static variable in interface wyil.lang.Type

Represents the set of (unbound) integer values.

T_META - Static variable in interface wyil.lang.Type

The type meta represents the type of types.

T_NULL - Static variable in interface wyil.lang.Type

The null type is a special type which should be used to show the absence of something.

T_VOID - Static variable in interface wyil.lang.Type

A void type represents the type whose variables cannot exist! That is, they cannot hold any possible value.

TestUtils - Class in wyc.util

TestUtils() - Constructor for class wyc.util.TestUtils

TestUtils.StreamGrabber - Class in wyc.util

Grab everything produced by a given input stream until the End-Of-File (EOF) is reached.

text - Variable in class wyc.io.WhileyFileLexer.Token

to - Variable in class wyil.util.type.SubtypeOperator

toAutomaton(Type) - Method in class wyil.util.TypeSystem

Expand a given type by inlining all visible nominal information.

toImplArrays(Type.Impl[]) - Static method in interface wyil.lang.Type

toImplOrVoid(Type[]) - Static method in interface wyil.lang.Type

toImplRecords(Type.Impl[]) - Static method in interface wyil.lang.Type

toIntegerList(int...) - Method in class wyc.builder.CodeGenerator

Token(WhileyFileLexer.Token.Kind, String, int) - Constructor for class wyc.io.WhileyFileLexer.Token

toSemanticType(WyalFile.Type, WhileyFile.Context) - Method in class wyc.builder.CompileTask

Convert a Whiley "syntactic" type into a wyil type.

toString() - Method in class wyautl_old.lang.Automaton

toString() - Method in class wyautl_old.util.BinaryMatrix

toString() - Method in enum wyc.io.WhileyFileLexer.Token.Kind

toString() - Method in class wyc.lang.Expr.AbstractVariable

toString() - Method in class wyc.lang.Expr.BinOp

toString() - Method in class wyc.lang.Expr.Cast

toString() - Method in class wyc.lang.Expr.Constant

toString() - Method in class wyc.lang.Expr.ConstantAccess

toString() - Method in class wyc.lang.Expr.Dereference

toString() - Method in class wyc.lang.Expr.FieldAccess

toString() - Method in class wyc.lang.Expr.IndexOf

toString() - Method in class wyc.lang.Expr.LocalVariable

toString() - Method in class wyc.lang.Expr.UnOp

toString() - Method in class wyc.lang.Stmt.Debug

toString() - Method in class wyc.lang.Stmt.Return

toString() - Method in class wyil.lang.Bytecode.AliasDeclaration

toString() - Method in class wyil.lang.Bytecode.Assert

toString() - Method in class wyil.lang.Bytecode.Assign

toString() - Method in class wyil.lang.Bytecode.Assume

toString() - Method in class wyil.lang.Bytecode.Block

toString() - Method in class wyil.lang.Bytecode.Break

toString() - Method in class wyil.lang.Bytecode.Const

toString() - Method in class wyil.lang.Bytecode.Continue

toString() - Method in class wyil.lang.Bytecode.Convert

toString() - Method in class wyil.lang.Bytecode.Debug

toString() - Method in class wyil.lang.Bytecode.DoWhile

toString() - Method in class wyil.lang.Bytecode.Fail

toString() - Method in class wyil.lang.Bytecode.FieldLoad

toString() - Method in class wyil.lang.Bytecode.If

toString() - Method in class wyil.lang.Bytecode.Index

toString() - Method in class wyil.lang.Bytecode.IndirectInvoke

toString() - Method in class wyil.lang.Bytecode.Invoke

toString() - Method in class wyil.lang.Bytecode.Lambda

toString() - Method in class wyil.lang.Bytecode.NamedBlock

toString() - Method in class wyil.lang.Bytecode.Operator

toString() - Method in class wyil.lang.Bytecode.Quantifier

toString() - Method in class wyil.lang.Bytecode.Return

toString() - Method in class wyil.lang.Bytecode.Schema

toString() - Method in class wyil.lang.Bytecode.Skip

toString() - Method in class wyil.lang.Bytecode.Switch

toString() - Method in class wyil.lang.Bytecode.VariableAccess

toString() - Method in class wyil.lang.Bytecode.VariableDeclaration

toString() - Method in class wyil.lang.Bytecode.While

toString() - Method in class wyil.lang.Constant.Array

toString() - Method in class wyil.lang.Constant.Bool

toString() - Method in class wyil.lang.Constant.Byte

toString() - Method in class wyil.lang.Constant.FunctionOrMethod

toString() - Method in class wyil.lang.Constant.Integer

toString() - Method in class wyil.lang.Constant.Null

toString() - Method in class wyil.lang.Constant.Record

toString() - Method in class wyil.lang.Constant.Type

toString() - Method in class wyil.lang.Modifier.Export

toString() - Method in class wyil.lang.Modifier.Native

toString() - Method in class wyil.lang.Modifier.Private

toString() - Method in class wyil.lang.Modifier.Public

toString() - Method in class wyil.lang.SyntaxTree.Location

toString() - Method in class wyil.lang.Type.Impl.Function

toString() - Method in class wyil.lang.Type.Impl.Method

toString() - Method in class wyil.lang.Type.Impl.Primitive

toString() - Method in class wyil.lang.Type.Impl.Property

toString() - Method in class wyil.util.type.LifetimeRelation

translate(WyilFile) - Method in class wyil.builders.VerificationConditionGenerator

Translate a WyilFile into a WyalFile which contains the verification conditions necessary to establish that all functions and methods in the WyilFile meet their specifications, and that no array-out-of-bounds or division-by-zero exceptions are possible (amongst other things).

True - Static variable in class wyil.lang.Constant

The Bool true constant

trueBranch - Variable in class wyc.lang.Stmt.IfElse

trueBranch() - Method in class wyil.lang.Bytecode.If

Return the block identifier for the true branch associated with this bytecode.

TRUEBRANCH - Static variable in class wyil.lang.SyntaxTree

type - Variable in class wyc.lang.Expr.AbstractFunctionOrMethod

type - Variable in class wyc.lang.Expr.ArrayGenerator

type - Variable in class wyc.lang.Expr.ArrayInitialiser

type - Variable in class wyc.lang.Expr.Cast

type - Variable in class wyc.lang.Expr.ConstantAccess

type() - Method in class wyc.lang.Expr.FunctionCall

type() - Method in class wyc.lang.Expr.FunctionOrMethodCall

type() - Method in class wyc.lang.Expr.IndirectFunctionCall

type() - Method in class wyc.lang.Expr.IndirectFunctionOrMethodCall

type() - Method in class wyc.lang.Expr.IndirectMethodCall

type - Variable in class wyc.lang.Expr.Lambda

type - Variable in class wyc.lang.Expr.LocalVariable

type() - Method in class wyc.lang.Expr.MethodCall

type - Variable in class wyc.lang.Expr.New

type() - Method in class wyc.lang.Expr.PropertyCall

type - Variable in class wyc.lang.Expr.Quantifier

type - Variable in class wyc.lang.Expr.Record

type - Variable in class wyc.lang.Expr.TypeVal

type - Variable in class wyc.lang.Expr.UnOp

type - Variable in class wyc.lang.Stmt.VariableDeclaration

type - Variable in class wyc.lang.WhileyFile.Parameter

Type(List<Modifier>, WhileyFile.Parameter, String, List<Expr>, Attribute...) - Constructor for class wyc.lang.WhileyFile.Type

type() - Method in class wyil.lang.Bytecode.IndirectInvoke

type() - Method in class wyil.lang.Bytecode.Invoke

type() - Method in class wyil.lang.Bytecode.Lambda

type() - Method in class wyil.lang.Constant.Array

type() - Method in class wyil.lang.Constant.Bool

type() - Method in class wyil.lang.Constant.Byte

type() - Method in class wyil.lang.Constant.FunctionOrMethod

type() - Method in class wyil.lang.Constant.Integer

type() - Method in class wyil.lang.Constant.Null

type() - Method in class wyil.lang.Constant.Record

type() - Method in class wyil.lang.Constant

Type(Type) - Constructor for class wyil.lang.Constant.Type

type() - Method in class wyil.lang.Constant.Type

Type - Interface in wyil.lang

A structural type.

type() - Method in class wyil.lang.WyilFile.FunctionOrMethodOrProperty

type(String) - Method in class wyil.lang.WyilFile

Looks up a type declaration in this WyilFile with the given name; if none exists, returns null.

Type(WyilFile, Collection<Modifier>, String, Type, Attribute...) - Constructor for class wyil.lang.WyilFile.Type

Type(WyilFile, Collection<Modifier>, String, Type, Collection<Attribute>) - Constructor for class wyil.lang.WyilFile.Type

type() - Method in class wyil.lang.WyilFile.Type

type() - Method in class wyil.util.interpreter.Interpreter.ConstantLambda

type() - Method in class wyil.util.interpreter.Interpreter.ConstantObject

Type.Array - Interface in wyil.lang

An array type describes array values whose elements are subtypes of the element type.

Type.EffectiveArray - Interface in wyil.lang

An effective array is a type which looks like an array, but is not exactly an array.

Type.EffectiveRecord - Interface in wyil.lang

An effective record is a type which looks like a record, but is not exactly a record.

Type.EffectiveReference - Interface in wyil.lang

An effective reference is a type which looks like an reference, but is not exactly an reference.

Type.Function - Interface in wyil.lang

Represents the set of all function values.

Type.FunctionOrMethod - Interface in wyil.lang

Represents the set of all functions or methods.

Type.Impl - Class in wyil.lang

Type.Impl.Atom - Class in wyil.lang

An atom represents an indivisible type.

Type.Impl.Conjunctable - Class in wyil.lang

Represents either an atom or a conjunct

Type.Impl.Function - Class in wyil.lang

A function type, consisting of a list of zero or more parameters and a return type.

Type.Impl.FunctionOrMethod - Class in wyil.lang

Type.Impl.Method - Class in wyil.lang

Type.Impl.PositiveAtom - Class in wyil.lang

A positive atom is any atom except a negation

Type.Impl.Primitive - Class in wyil.lang

Type.Impl.Property - Class in wyil.lang

Type.Intersection - Interface in wyil.lang

Represents the intersection of one or more types together.

Type.Leaf - Interface in wyil.lang

Represents a type which constitutes a "leaf" node in the type tree.

Type.Method - Interface in wyil.lang

Represents the set of all method values.

Type.Negation - Interface in wyil.lang

Represents the set of types which are not in a given type.

Type.Nominal - Interface in wyil.lang

Represents a named type within the system.

Type.Primitive - Interface in wyil.lang

Represents a primitive type (e.g.

Type.Property - Interface in wyil.lang

Represents the set of all proeprty values.

Type.Record - Interface in wyil.lang

A record is made up of a number of fields, each of which has a unique name.

Type.Reference - Interface in wyil.lang

Represents a reference to an object in Whiley.

Type.Union - Interface in wyil.lang

Represents the union of one or more types together.

TYPE_Any - Static variable in class wyil.io.WyilFileWriter

TYPE_Array - Static variable in class wyil.io.WyilFileWriter

TYPE_Bool - Static variable in class wyil.io.WyilFileWriter

TYPE_Byte - Static variable in class wyil.io.WyilFileWriter

TYPE_Function - Static variable in class wyil.io.WyilFileWriter

TYPE_Int - Static variable in class wyil.io.WyilFileWriter

TYPE_Intersection - Static variable in class wyil.io.WyilFileWriter

TYPE_Method - Static variable in class wyil.io.WyilFileWriter

TYPE_Negation - Static variable in class wyil.io.WyilFileWriter

TYPE_Nominal - Static variable in class wyil.io.WyilFileWriter

TYPE_Null - Static variable in class wyil.io.WyilFileWriter

TYPE_Property - Static variable in class wyil.io.WyilFileWriter

TYPE_Record - Static variable in class wyil.io.WyilFileWriter

TYPE_Reference - Static variable in class wyil.io.WyilFileWriter

TYPE_Type - Static variable in class wyil.io.WyilFileWriter

TYPE_Union - Static variable in class wyil.io.WyilFileWriter

TYPE_Void - Static variable in class wyil.io.WyilFileWriter

TypeAlgorithms - Class in wyil.util.type

Contains various important algorithms for manipulating types.

TypeAlgorithms() - Constructor for class wyil.util.type.TypeAlgorithms

typeDecl(String) - Method in class wyc.lang.WhileyFile

TypeParser - Class in wyil.util.type

The Type Parser is used to convert a given string into a type (or a syntax error).

TypeParser(String) - Constructor for class wyil.util.type.TypeParser

types() - Method in class wyil.lang.WyilFile

Returns all type declarations in this WyilFile.

TypeSystem - Class in wyil.util

The type system is responsible for managing the relationship between nominal types and their underlying types.

TypeSystem(Build.Project) - Constructor for class wyil.util.TypeSystem

TypeSystem.FunctionOrMethodState - Class in wyil.util

TypeSystem.RecordState - Class in wyil.util

TypeVal(WyalFile.Type, Attribute...) - Constructor for class wyc.lang.Expr.TypeVal

U

UC_ELEMENTOF - Static variable in class wyc.io.WhileyFileLexer

UC_EMPTYSET - Static variable in class wyc.io.WhileyFileLexer

UC_EXISTS - Static variable in class wyc.io.WhileyFileLexer

UC_FORALL - Static variable in class wyc.io.WhileyFileLexer

UC_GREATEREQUALS - Static variable in class wyc.io.WhileyFileLexer

UC_LESSEQUALS - Static variable in class wyc.io.WhileyFileLexer

UC_LOGICALAND - Static variable in class wyc.io.WhileyFileLexer

UC_LOGICALOR - Static variable in class wyc.io.WhileyFileLexer

UC_SETINTERSECTION - Static variable in class wyc.io.WhileyFileLexer

UC_SETUNION - Static variable in class wyc.io.WhileyFileLexer

UC_SUBSET - Static variable in class wyc.io.WhileyFileLexer

UC_SUBSETEQ - Static variable in class wyc.io.WhileyFileLexer

UC_SUPSET - Static variable in class wyc.io.WhileyFileLexer

UC_SUPSETEQ - Static variable in class wyc.io.WhileyFileLexer

UNARY_ASSIGNABLE - Static variable in interface wyil.lang.Bytecode

UNARY_OPERATOR - Static variable in interface wyil.lang.Bytecode

Union(Type...) - Static method in interface wyil.lang.Type

Construct the union of one or more types together.

UNKNOWN_FUNCTION_OR_METHOD - Static variable in class wyil.util.ErrorMessages

UNKNOWN_VARIABLE - Static variable in class wyil.util.ErrorMessages

UnOp(Expr.UOp, Expr, Attribute...) - Constructor for class wyc.lang.Expr.UnOp

UNREACHABLE_CODE - Static variable in class wyil.util.ErrorMessages

unresolvedType - Variable in class wyc.lang.Expr.Cast

unresolvedType - Variable in class wyc.lang.Expr.TypeVal

unresolvedType() - Method in class wyc.lang.WhileyFile.Function

unresolvedType() - Method in class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

unresolvedType() - Method in class wyc.lang.WhileyFile.Method

unresolvedType() - Method in class wyc.lang.WhileyFile.Property

update(Type) - Method in interface wyil.lang.Type.EffectiveArray

Determine a new type for this array after an assignment to a given element.

update(String, Type) - Method in interface wyil.lang.Type.EffectiveRecord

Get an updated version of this record type after a given field has been assigned a given type.

uses(Expr, WhileyFile.Context) - Static method in class wyc.lang.Exprs

Determine the set of variable names (and their types) used in a given expression.

Util() - Constructor for class wyil.lang.Bytecode.Util

V

value - Variable in class wyc.lang.Expr.Constant

value - Variable in class wyc.lang.Expr.ConstantAccess

value() - Method in class wyil.lang.Constant.Bool

value() - Method in class wyil.lang.Constant.Byte

value() - Method in class wyil.lang.Constant.Integer

value() - Method in class wyil.lang.Constant.Type

valueOf(String) - Static method in enum wyc.commands.Compile.Result

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyc.commands.Decompile.Result

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyc.commands.Run.Result

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyc.io.WhileyFileLexer.Token.Kind

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyc.lang.Expr.BOp

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyc.lang.Expr.QOp

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyc.lang.Expr.UOp

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyil.lang.Bytecode.Blocks

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyil.lang.Bytecode.Extras

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyil.lang.Bytecode.OperandGroups

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyil.lang.Bytecode.Operands

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyil.lang.Bytecode.OperatorKind

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum wyil.lang.Bytecode.QuantifierKind

Returns the enum constant of this type with the specified name.

values() - Static method in enum wyc.commands.Compile.Result

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyc.commands.Decompile.Result

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyc.commands.Run.Result

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyc.io.WhileyFileLexer.Token.Kind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyc.lang.Expr.BOp

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyc.lang.Expr.QOp

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyc.lang.Expr.UOp

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyil.lang.Bytecode.Blocks

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Method in class wyil.lang.Bytecode.Case

values() - Static method in enum wyil.lang.Bytecode.Extras

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyil.lang.Bytecode.OperandGroups

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyil.lang.Bytecode.Operands

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyil.lang.Bytecode.OperatorKind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum wyil.lang.Bytecode.QuantifierKind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Method in class wyil.lang.Constant.Array

values() - Method in class wyil.lang.Constant.Record

var - Variable in class wyc.lang.Expr.AbstractVariable

variable() - Method in class wyil.lang.Bytecode.Range

Return the location index for the variable this range is declaring.

VARIABLE - Static variable in class wyil.lang.SyntaxTree

VARIABLE_ALREADY_DEFINED - Static variable in class wyil.util.ErrorMessages

VARIABLE_POSSIBLY_UNITIALISED - Static variable in class wyil.util.ErrorMessages

VariableAccess(boolean, int) - Constructor for class wyil.lang.Bytecode.VariableAccess

VariableDeclaration(WhileyFile.Parameter, Expr, Attribute...) - Constructor for class wyc.lang.Stmt.VariableDeclaration

Construct a variable declaration from a given type, variable name and optional initialiser expression.

VariableDeclaration(WhileyFile.Parameter, Expr, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.VariableDeclaration

Construct a variable declaration from a given type, variable name and optional initialiser expression.

VariableDeclaration(String) - Constructor for class wyil.lang.Bytecode.VariableDeclaration

VariableDeclaration(String, int) - Constructor for class wyil.lang.Bytecode.VariableDeclaration

verbose - Variable in class wyc.commands.Compile

Signals that verbose output should be produced.

VerificationConditionGenerator - Class in wyil.builders

Responsible for generating verification conditions from a given WyIL file.

VerificationConditionGenerator(WyalFile, Wyil2WyalBuilder) - Constructor for class wyil.builders.VerificationConditionGenerator

verificationConditions - Variable in class wyc.commands.Compile

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

verify - Variable in class wyc.commands.Compile

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

W

While(Expr, List<Expr>, Collection<Stmt>, Attribute...) - Constructor for class wyc.lang.Stmt.While

Construct a While statement from a given condition and body of statements.

While(Expr, List<Expr>, Collection<Stmt>, Collection<Attribute>) - Constructor for class wyc.lang.Stmt.While

Construct a While statement from a given condition and body of statements.

While(int, int, int[], int[]) - Constructor for class wyil.lang.Bytecode.While

whileydir - Variable in class wyc.util.AbstractProjectCommand

The location in which whiley source files a located, or null if not specified.

whileyExcludes - Variable in class wyc.commands.Compile

Identifies which whiley sources files should not be considered for compilation.

WhileyFile - Class in wyc.lang

Provides classes representing the various kinds of declaration found in a Whiley source file.

WhileyFile(Path.Entry<WhileyFile>) - Constructor for class wyc.lang.WhileyFile

WhileyFile.Constant - Class in wyc.lang

Represents a constant declaration in a Whiley source file, which has the form:

WhileyFile.Context - Interface in wyc.lang

WhileyFile.Declaration - Interface in wyc.lang

WhileyFile.Function - Class in wyc.lang

Represents a function declaration in a Whiley source file.

WhileyFile.FunctionOrMethodOrProperty - Class in wyc.lang

Represents a function declaration or method declaration in a Whiley source file which have the form:

WhileyFile.Import - Class in wyc.lang

Represents an import declaration in a Whiley source file, which has the form:

WhileyFile.Method - Class in wyc.lang

Represents a method declaration in a Whiley source file.

WhileyFile.NamedDeclaration - Class in wyc.lang

WhileyFile.Parameter - Class in wyc.lang

Represents a parameter declaration as part of a function or method declaration.

WhileyFile.Property - Class in wyc.lang

Represents a function declaration in a Whiley source file.

WhileyFile.Type - Class in wyc.lang

Represents a type declaration in a Whiley source file, which has the form:

WhileyFileLexer - Class in wyc.io

Split a source file into a list of tokens.

WhileyFileLexer(Path.Entry<WhileyFile>) - Constructor for class wyc.io.WhileyFileLexer

WhileyFileLexer.Token - Class in wyc.io

The base class for all tokens.

WhileyFileLexer.Token.Kind - Enum in wyc.io

WhileyFileParser - Class in wyc.io

Convert a list of tokens into an Abstract Syntax Tree (AST) representing the original source file in question.

WhileyFileParser(Path.Entry<WhileyFile>, List<WhileyFileLexer.Token>) - Constructor for class wyc.io.WhileyFileParser

WhileyFilePrinter - Class in wyc.io

Responsible for "pretty printing" a Whiley File.

WhileyFilePrinter(OutputStream) - Constructor for class wyc.io.WhileyFilePrinter

whileyIncludes - Variable in class wyc.commands.Compile

Identifies which whiley source files should be considered for compilation.

whileypath - Variable in class wyc.util.AbstractProjectCommand

The whiley path identifies additional items (i.e.

write(Automaton) - Method in class wyautl_old.io.BinaryAutomataWriter

write(Automaton.State) - Method in class wyautl_old.io.BinaryAutomataWriter

write(T) - Method in interface wyautl_old.io.GenericWriter

write(WyilFile) - Method in class wyil.io.WyilFileWriter

write(Constant) - Method in class wyil.util.interpreter.Interpreter.ConstantObject

write(Automaton.State) - Method in class wyil.util.type.BinaryTypeWriter

writer - Variable in class wyautl_old.io.BinaryAutomataWriter

wyaldir - Variable in class wyc.util.AbstractProjectCommand

The location in which wyal source files are stored, or null if not specified.

wyautl_old - package wyautl_old

The Whiley Automata Library.

wyautl_old.io - package wyautl_old.io

Provides classes for reading and writing automata via input/output streams.

wyautl_old.lang - package wyautl_old.lang

Provides core classes for representing and manipulating automata.

wyautl_old.util - package wyautl_old.util

Provides various utility classes, primarily for generating and testing automata.

wyc - package wyc

The Whiley Compiler Front End.

wyc.builder - package wyc.builder

Provides the classes responsible for actually translating WhileyFiles into WyilFiles.

wyc.commands - package wyc.commands

wyc.io - package wyc.io

wyc.lang - package wyc.lang

Provides core classes for the Abstract Syntax Tree (AST) used to represent Whiley source files.

wyc.util - package wyc.util

wycsdir - Variable in class wyc.util.AbstractProjectCommand

The location in which wycs binary files are stored, or null if not specified.

wyil - package wyil

The Whiley Intermediate Language (WYIL).

wyil.builders - package wyil.builders

wyil.checks - package wyil.checks

Provides classes responsible for validity checking of WYIL modules.

wyil.io - package wyil.io

Provides classes for handling reading/writing WYIL modules.

wyil.lang - package wyil.lang

Provides core classes for representing WYIL modules and bytecodes.

wyil.util - package wyil.util

wyil.util.interpreter - package wyil.util.interpreter

wyil.util.type - package wyil.util.type

Wyil2WyalBuilder - Class in wyil.builders

Responsible for converting a Wyil file into a Wycs file which can then be passed into the Whiley Constraint Solver (Wycs).

Wyil2WyalBuilder(Build.Project) - Constructor for class wyil.builders.Wyil2WyalBuilder

wyildir - Variable in class wyc.util.AbstractProjectCommand

The location in which wyil binary files are stored, or null if not specified.

wyilExcludes - Variable in class wyc.commands.Compile

Identifies which wyil sources files should not be considered for compilation.

WyilFile - Class in wyil.lang

Provides an in-memory representation of a binary WyIL file.

WyilFile(Path.Entry<? extends CompilationUnit>) - Constructor for class wyil.lang.WyilFile

Construct a WyilFile objects with a given identifier, originating filename and list of declarations.

WyilFile.Block - Class in wyil.lang

A block is an chunk of information within a WyIL file.

WyilFile.Constant - Class in wyil.lang

A constant declaration is a top-level block within a WyilFile that associates a name with a given constant value.

WyilFile.Declaration - Class in wyil.lang

A declaration is a named entity within a WyIL file, and is either a type, constant, function or method declaration.

WyilFile.FunctionOrMethod - Class in wyil.lang

WyilFile.FunctionOrMethodOrProperty - Class in wyil.lang

WyilFile.Property - Class in wyil.lang

WyilFile.Type - Class in wyil.lang

A type declaration is a top-level block within a WyilFile that associates a name with a given type.

WyilFilePrinter - Class in wyil.io

Writes WYIL bytecodes in a textual from to a given file.

WyilFilePrinter(Build.Task) - Constructor for class wyil.io.WyilFilePrinter

WyilFilePrinter(PrintWriter) - Constructor for class wyil.io.WyilFilePrinter

WyilFilePrinter(OutputStream) - Constructor for class wyil.io.WyilFilePrinter

WyilFileReader - Class in wyil.io

Read a binary WYIL file from a byte stream and convert into the corresponding WyilFile object.

WyilFileReader(Path.Entry<WyilFile>) - Constructor for class wyil.io.WyilFileReader

WyilFileReader(InputStream) - Constructor for class wyil.io.WyilFileReader

Construct a WyilFileReader to read a WyilFile in headless mode.

WyilFileWriter - Class in wyil.io

Responsible for writing a WyilFile to an output stream in binary form.

WyilFileWriter(OutputStream) - Constructor for class wyil.io.WyilFileWriter

wyilIncludes - Variable in class wyc.commands.Compile

Identifies which wyil source files should be considered for compilation.

A B C D E F G H I K L M N O P Q R S T U V W