| Package | Description |
|---|---|
| wyc.builder |
Provides the classes responsible for actually translating WhileyFiles into WyilFiles.
|
| wyc.io | |
| wyc.lang |
Provides core classes for the Abstract Syntax Tree (AST) used to represent Whiley source files.
|
| Modifier and Type | Method and Description |
|---|---|
Expr |
FlowTypeChecker.propagate(Expr expr,
wyc.builder.FlowTypeChecker.Environment environment,
WhileyFile.Context context)
Propagate types through a given expression, whilst checking that it is
well typed.
|
| Modifier and Type | Method and Description |
|---|---|
wycc.util.Pair<Expr,wyc.builder.FlowTypeChecker.Environment> |
FlowTypeChecker.propagateCondition(Expr expr,
boolean sign,
wyc.builder.FlowTypeChecker.Environment environment,
WhileyFile.Context context)
Propagate type information through an expression being used as a
condition, whilst checking it is well-typed at the same time.
|
| Modifier and Type | Method and Description |
|---|---|
Type.EffectiveArray |
FlowTypeChecker.expandAsEffectiveArray(Expr src,
WhileyFile.Context context) |
Type.FunctionOrMethod |
FlowTypeChecker.expandAsEffectiveFunctionOrMethod(Expr src,
WhileyFile.Context context) |
Type.EffectiveRecord |
FlowTypeChecker.expandAsEffectiveRecord(Expr src,
WhileyFile.Context context) |
Type.Reference |
FlowTypeChecker.expandAsEffectiveReference(Expr src,
WhileyFile.Context context) |
wyc.builder.CodeGenerator.FlowResult |
CodeGenerator.generateCondition(Expr condition,
wyc.builder.CodeGenerator.EnclosingScope scope)
Translate a source-level conditional expression into WyIL bytecodes,
using a given scope mapping named variables to locations.
|
int |
CodeGenerator.generateExpression(Expr expression,
wyc.builder.CodeGenerator.EnclosingScope scope)
Translate a source-level expression into a WYIL bytecode block, using a
given environment mapping named variables to registers.
|
Expr |
FlowTypeChecker.propagate(Expr expr,
wyc.builder.FlowTypeChecker.Environment environment,
WhileyFile.Context context)
Propagate types through a given expression, whilst checking that it is
well typed.
|
wycc.util.Pair<Expr,wyc.builder.FlowTypeChecker.Environment> |
FlowTypeChecker.propagateCondition(Expr expr,
boolean sign,
wyc.builder.FlowTypeChecker.Environment environment,
WhileyFile.Context context)
Propagate type information through an expression being used as a
condition, whilst checking it is well-typed at the same time.
|
wycc.util.Pair<Constant,Type> |
FlowTypeChecker.resolveAsConstant(Expr e,
WhileyFile.Context context)
Resolve a given constant expression as a constant value.
|
| Modifier and Type | Method and Description |
|---|---|
int[] |
CodeGenerator.generateMultipleReturns(List<Expr> expressions,
wyc.builder.CodeGenerator.EnclosingScope scope)
Translate a source-level expression into a WyIL bytecode block, using a
given environment mapping named variables to registers.
|
| Modifier and Type | Method and Description |
|---|---|
List<Expr> |
WhileyFileParser.parseExpressions(WhileyFile wf,
wyc.io.WhileyFileParser.EnclosingScope scope,
boolean terminated)
Parse a "multi-expression"; that is, a sequence of one or more
expressions separated by comma's
|
| Modifier and Type | Method and Description |
|---|---|
void |
WhileyFilePrinter.print(Expr expression) |
void |
WhileyFilePrinter.printWithBrackets(Expr expression,
Class<? extends Expr>... matches) |
| Modifier and Type | Interface and Description |
|---|---|
static interface |
Expr.LVal
An LVal is a special form of expression which may appear on the left-hand
side of an assignment.
|
| Modifier and Type | Class and Description |
|---|---|
static class |
Expr.AbstractFunctionOrMethod |
static class |
Expr.AbstractIndirectInvoke |
static class |
Expr.AbstractInvoke |
static class |
Expr.AbstractVariable |
static class |
Expr.ArrayGenerator
Represents an array generator expression, which is of the form:
|
static class |
Expr.ArrayInitialiser
Represents an array initialiser expression, which is of the form:
|
static class |
Expr.AssignedVariable |
static class |
Expr.BinOp |
static class |
Expr.Cast
Represents a cast expression, which has the form:
|
static class |
Expr.Constant |
static class |
Expr.ConstantAccess |
static class |
Expr.Dereference |
static class |
Expr.FieldAccess |
static class |
Expr.FunctionCall
Parse a function invocation expression, which has the form:
|
static class |
Expr.FunctionOrMethod |
static class |
Expr.FunctionOrMethodCall |
static class |
Expr.IndexOf |
static class |
Expr.IndirectFunctionCall |
static class |
Expr.IndirectFunctionOrMethodCall |
static class |
Expr.IndirectMethodCall |
static class |
Expr.Lambda |
static class |
Expr.LocalVariable |
static class |
Expr.MethodCall |
static class |
Expr.New |
static class |
Expr.PropertyCall |
static class |
Expr.Quantifier |
static class |
Expr.Record |
static class |
Expr.TypeVal |
static class |
Expr.UnOp |
| Modifier and Type | Field and Description |
|---|---|
Expr |
Expr.Lambda.body |
Expr |
Stmt.While.condition |
Expr |
Stmt.DoWhile.condition |
Expr |
Stmt.IfElse.condition |
Expr |
Expr.Quantifier.condition |
Expr |
WhileyFile.Constant.constant |
Expr |
Expr.ArrayGenerator.count |
Expr |
Expr.ArrayGenerator.element |
Expr |
Stmt.Assert.expr |
Expr |
Stmt.Assume.expr |
Expr |
Stmt.VariableDeclaration.expr |
Expr |
Stmt.Switch.expr |
Expr |
Stmt.Debug.expr |
Expr |
Expr.Cast.expr |
Expr |
Expr.New.expr |
Expr |
Expr.IndexOf.index |
Expr |
Expr.BinOp.lhs |
Expr |
Expr.UnOp.mhs |
Expr |
Expr.BinOp.rhs |
Expr |
Expr.IndexOf.src |
Expr |
Expr.FieldAccess.src |
Expr |
Expr.Dereference.src |
Expr |
Expr.AbstractIndirectInvoke.src |
| Modifier and Type | Field and Description |
|---|---|
ArrayList<Expr> |
Expr.ArrayInitialiser.arguments |
ArrayList<Expr> |
Expr.AbstractInvoke.arguments |
ArrayList<Expr> |
Expr.AbstractIndirectInvoke.arguments |
List<Expr> |
WhileyFile.FunctionOrMethodOrProperty.ensures |
ArrayList<Expr> |
Stmt.Case.expr |
HashMap<String,Expr> |
Expr.Record.fields |
ArrayList<Expr> |
WhileyFile.Type.invariant |
List<Expr> |
Stmt.While.invariants |
ArrayList<Expr> |
Stmt.DoWhile.invariants |
List<Expr> |
WhileyFile.FunctionOrMethodOrProperty.requires |
ArrayList<Expr> |
Stmt.Return.returns |
List<Expr> |
Stmt.Assign.rvals |
ArrayList<wycc.util.Triple<String,Expr,Expr>> |
Expr.Quantifier.sources |
ArrayList<wycc.util.Triple<String,Expr,Expr>> |
Expr.Quantifier.sources |
| Modifier and Type | Method and Description |
|---|---|
static boolean |
Exprs.isPure(Expr expr,
WhileyFile.Context context)
Determine whether this expression is "pure" or not.
|
static HashSet<wycc.util.Pair<Type,String>> |
Exprs.uses(Expr expr,
WhileyFile.Context context)
Determine the set of variable names (and their types) used in a given expression.
|
| Constructor and Description |
|---|
AbstractIndirectInvoke(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
AbstractIndirectInvoke(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
ArrayGenerator(Expr element,
Expr count,
wybs.lang.Attribute... attributes) |
ArrayInitialiser(wybs.lang.Attribute attribute,
Expr... arguments) |
Assert(Expr expr,
wybs.lang.Attribute... attributes)
Create a given assert statement.
|
Assert(String msg,
Expr expr,
Collection<wybs.lang.Attribute> attributes)
Create a given assert statement.
|
Assume(Expr expr,
wybs.lang.Attribute... attributes)
Create a given assume statement.
|
Assume(String msg,
Expr expr,
Collection<wybs.lang.Attribute> attributes)
Create a given assume statement.
|
BinOp(Expr.BOp op,
Expr lhs,
Expr rhs,
wybs.lang.Attribute... attributes) |
BinOp(Expr.BOp op,
Expr lhs,
Expr rhs,
Collection<wybs.lang.Attribute> attributes) |
Cast(wyal.lang.WyalFile.Type type,
Expr expr,
wybs.lang.Attribute... attributes) |
Constant(List<Modifier> modifiers,
Expr constant,
String name,
wybs.lang.Attribute... attributes) |
Debug(Expr expr,
wybs.lang.Attribute... attributes) |
Debug(Expr expr,
Collection<wybs.lang.Attribute> attributes) |
Dereference(Expr src,
wybs.lang.Attribute... attributes) |
DoWhile(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
wybs.lang.Attribute... attributes)
Construct a Do-While statement from a given condition and body of
statements.
|
DoWhile(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
Collection<wybs.lang.Attribute> attributes)
Construct a Do-While statement from a given condition and body of
statements.
|
FieldAccess(Expr lhs,
String name,
wybs.lang.Attribute... attributes) |
FieldAccess(Expr lhs,
String name,
Collection<wybs.lang.Attribute> attributes) |
IfElse(Expr condition,
List<Stmt> trueBranch,
List<Stmt> falseBranch,
wybs.lang.Attribute... attributes)
Construct an if-else statement from a condition, true branch and
optional false branch.
|
IfElse(Expr condition,
List<Stmt> trueBranch,
List<Stmt> falseBranch,
Collection<wybs.lang.Attribute> attributes)
Construct an if-else statement from a condition, true branch and
optional false branch.
|
IndexOf(Expr src,
Expr index,
wybs.lang.Attribute... attributes) |
IndexOf(Expr src,
Expr index,
Collection<wybs.lang.Attribute> attributes) |
IndirectFunctionCall(Expr src,
Collection<Expr> arguments,
wybs.lang.Attribute... attributes) |
IndirectFunctionCall(Expr src,
Collection<Expr> arguments,
Collection<wybs.lang.Attribute> attributes) |
IndirectFunctionOrMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
IndirectFunctionOrMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
IndirectMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
IndirectMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
Lambda(Collection<WhileyFile.Parameter> parameters,
Collection<String> contextLifetimes,
Collection<String> lifetimeParameters,
Expr body,
wybs.lang.Attribute... attributes) |
Lambda(Collection<WhileyFile.Parameter> parameters,
Collection<String> contextLifetimes,
Collection<String> lifetimeParameters,
Expr body,
Collection<wybs.lang.Attribute> attributes) |
New(Expr expr,
String lifetime,
wybs.lang.Attribute... attributes) |
Quantifier(Expr.QOp cop,
Collection<wycc.util.Triple<String,Expr,Expr>> sources,
Expr condition,
wybs.lang.Attribute... attributes) |
Switch(Expr condition,
List<Stmt.Case> cases,
wybs.lang.Attribute... attributes) |
Switch(Expr condition,
List<Stmt.Case> cases,
Collection<wybs.lang.Attribute> attributes) |
UnOp(Expr.UOp op,
Expr mhs,
wybs.lang.Attribute... attributes) |
VariableDeclaration(WhileyFile.Parameter parameter,
Expr expr,
wybs.lang.Attribute... attributes)
Construct a variable declaration from a given type, variable name and
optional initialiser expression.
|
VariableDeclaration(WhileyFile.Parameter parameter,
Expr expr,
Collection<wybs.lang.Attribute> attributes)
Construct a variable declaration from a given type, variable name and
optional initialiser expression.
|
While(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
wybs.lang.Attribute... attributes)
Construct a While statement from a given condition and body of
statements.
|
While(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
Collection<wybs.lang.Attribute> attributes)
Construct a While statement from a given condition and body of
statements.
|
| Constructor and Description |
|---|
AbstractIndirectInvoke(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
AbstractIndirectInvoke(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
AbstractInvoke(String name,
wyfs.lang.Path.ID receiver,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
AbstractInvoke(String name,
wyfs.lang.Path.ID receiver,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
ArrayInitialiser(Collection<Expr> arguments,
wybs.lang.Attribute... attributes) |
Assign(List<Expr.LVal> lvals,
List<Expr> rvals,
wybs.lang.Attribute... attributes)
Create an assignment from a given sequence of lvals and expressions on the right-hand side.
|
Assign(List<Expr.LVal> lvals,
List<Expr> rvals,
Collection<wybs.lang.Attribute> attributes)
Create an assignment from a given sequence of lvals and expressions on the right-hand side.
|
Case(List<Expr> values,
List<Stmt> statements,
wybs.lang.Attribute... attributes) |
DoWhile(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
wybs.lang.Attribute... attributes)
Construct a Do-While statement from a given condition and body of
statements.
|
DoWhile(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
Collection<wybs.lang.Attribute> attributes)
Construct a Do-While statement from a given condition and body of
statements.
|
Function(List<Modifier> modifiers,
String name,
List<WhileyFile.Parameter> returns,
List<WhileyFile.Parameter> parameters,
List<Expr> requires,
List<Expr> ensures,
List<Stmt> statements,
wybs.lang.Attribute... attributes) |
Function(List<Modifier> modifiers,
String name,
List<WhileyFile.Parameter> returns,
List<WhileyFile.Parameter> parameters,
List<Expr> requires,
List<Expr> ensures,
List<Stmt> statements,
wybs.lang.Attribute... attributes) |
FunctionCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
wybs.lang.Attribute... attributes) |
FunctionCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
Collection<wybs.lang.Attribute> attributes) |
FunctionOrMethodCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
FunctionOrMethodCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
FunctionOrMethodOrProperty(List<Modifier> modifiers,
String name,
List<WhileyFile.Parameter> returns,
List<WhileyFile.Parameter> parameters,
List<String> lifetimeParameters,
List<Expr> requires,
List<Expr> ensures,
List<Stmt> statements,
wybs.lang.Attribute... attributes)
Construct an object representing a Whiley function.
|
FunctionOrMethodOrProperty(List<Modifier> modifiers,
String name,
List<WhileyFile.Parameter> returns,
List<WhileyFile.Parameter> parameters,
List<String> lifetimeParameters,
List<Expr> requires,
List<Expr> ensures,
List<Stmt> statements,
wybs.lang.Attribute... attributes)
Construct an object representing a Whiley function.
|
IndirectFunctionCall(Expr src,
Collection<Expr> arguments,
wybs.lang.Attribute... attributes) |
IndirectFunctionCall(Expr src,
Collection<Expr> arguments,
Collection<wybs.lang.Attribute> attributes) |
IndirectFunctionOrMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
IndirectFunctionOrMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
IndirectMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
IndirectMethodCall(Expr src,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
Method(List<Modifier> modifiers,
String name,
List<WhileyFile.Parameter> returns,
List<WhileyFile.Parameter> parameters,
List<String> lifetimeParameters,
List<Expr> requires,
List<Expr> ensures,
List<Stmt> statements,
wybs.lang.Attribute... attributes) |
Method(List<Modifier> modifiers,
String name,
List<WhileyFile.Parameter> returns,
List<WhileyFile.Parameter> parameters,
List<String> lifetimeParameters,
List<Expr> requires,
List<Expr> ensures,
List<Stmt> statements,
wybs.lang.Attribute... attributes) |
MethodCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
wybs.lang.Attribute... attributes) |
MethodCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
Collection<String> lifetimeArguments,
Collection<wybs.lang.Attribute> attributes) |
Property(List<Modifier> modifiers,
String name,
List<WhileyFile.Parameter> parameters,
List<Expr> invariant,
wybs.lang.Attribute... attributes) |
PropertyCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
wybs.lang.Attribute... attributes) |
PropertyCall(wybs.lang.NameID nid,
wyfs.lang.Path.ID qualification,
Collection<Expr> arguments,
Collection<wybs.lang.Attribute> attributes) |
Quantifier(Expr.QOp cop,
Collection<wycc.util.Triple<String,Expr,Expr>> sources,
Expr condition,
wybs.lang.Attribute... attributes) |
Quantifier(Expr.QOp cop,
Collection<wycc.util.Triple<String,Expr,Expr>> sources,
Expr condition,
wybs.lang.Attribute... attributes) |
Record(String name,
Map<String,Expr> fields,
wybs.lang.Attribute... attributes) |
Return(List<Expr> returns,
wybs.lang.Attribute... attributes)
Create a given return statement with an optional return value.
|
Return(List<Expr> returns,
Collection<wybs.lang.Attribute> attributes)
Create a given return statement with an optional return value.
|
Type(List<Modifier> modifiers,
WhileyFile.Parameter type,
String name,
List<Expr> constraint,
wybs.lang.Attribute... attributes) |
While(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
wybs.lang.Attribute... attributes)
Construct a While statement from a given condition and body of
statements.
|
While(Expr condition,
List<Expr> invariants,
Collection<Stmt> body,
Collection<wybs.lang.Attribute> attributes)
Construct a While statement from a given condition and body of
statements.
|
Copyright © 2017. All rights reserved.