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

A

AbstractTransformer - Class in forge.transform

Implementation support for a transformer of a single call graph.

AbstractTransformer() - Constructor for class forge.transform.AbstractTransformer

Constructs a transformer with a tag that will be appended to each transformed procedure.

AbstractTransformer.TransformVisitor - Class in forge.transform

A TransformVisitor

AbstractTransformer.TransformVisitor(AbstractTransformer, ForgeCFG) - Constructor for class forge.transform.AbstractTransformer.TransformVisitor

Constructs a TransformVisitor belonging to the given transformer,

AbstractTransformer.TransformVisitor(AbstractTransformer, ForgeCFG, ForgeCFG.Impl) - Constructor for class forge.transform.AbstractTransformer.TransformVisitor

accept(CFGVisitor) - Method in class forge.cfg.AssignStmt

accept(CFGVisitor) - Method in class forge.cfg.BranchStmt

accept(CFGVisitor) - Method in class forge.cfg.CallStmt

accept(CFGVisitor) - Method in class forge.cfg.CFGStmt

Applies a CFG visitor to this stmt.

accept(CFGVisitor) - Method in class forge.cfg.CreateStmt

accept(CFGVisitor) - Method in class forge.cfg.ExitStmt

accept(CFGVisitor) - Method in class forge.cfg.SpecStmt

accept(ExpressionVisitor<T>) - Method in class forge.program.BinaryExpression

accept(ExpressionVisitor<T>) - Method in class forge.program.ConditionalExpression

accept(ExpressionVisitor<T>) - Method in interface forge.program.ForgeExpression

Accept a visitor.

accept(ExpressionVisitor<T>) - Method in class forge.program.ForgeLiteral

accept(ExpressionVisitor<T>) - Method in class forge.program.ForgeVariable

accept(ExpressionVisitor<T>) - Method in class forge.program.OldExpression

accept(ExpressionVisitor<T>) - Method in class forge.program.ProjectionExpression

accept(ExpressionVisitor<T>) - Method in class forge.program.QuantifyExpression

accept(ExpressionVisitor<T>) - Method in class forge.program.UnaryExpression

add(CFGStmt) - Method in class forge.cfg.StmtSet

addAll(Collection<? extends CFGStmt>) - Method in class forge.cfg.StmtSet

ANALYSIS - Static variable in class forge.dataflow.DominatorAnalysis

singleton.

ANALYSIS - Static variable in class forge.dataflow.InverseDominatorAnalysis

singleton.

ANALYSIS - Static variable in class forge.dataflow.ReachabilityAnalysis

singleton.

AnalysisResults<D> - Class in forge.dataflow

The results of a dataflow analysis.

analyze(ForgeCFG) - Method in class forge.dataflow.DataflowAnalysis

Performs the analysis and returns a mapping from each reachable node to the data at the program point immediately preceding the node.

and(ForgeExpression) - Method in interface forge.program.ForgeExpression

and(LocalVariable) - Method in interface forge.program.LocalDecls

Returns this decl appended with the given local.

and(LocalVariable) - Method in class forge.program.LocalDecls.EmptyDecls

and(LocalVariable) - Method in class forge.program.LocalDecls.MultiDecls

and(LocalVariable) - Method in class forge.program.LocalVariable

appendUpdate(StringBuilder) - Method in class forge.cfg.SpecStmt

apply(UnaryExpression.Op) - Method in interface forge.program.ForgeExpression

apply(UnaryExpression.Op) - Method in class forge.program.UnaryExpression

apply(CFGStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

arity() - Method in interface forge.program.ForgeExpression

Returns the arity of this expression.

arity() - Method in interface forge.solve.ForgeConstant

Returns the arity of this constant.

AssignStmt - Class in forge.cfg

A stmt which assigns an expression to a variable (local or field).

assumes() - Method in class forge.translate.ForgeTranslation

Returns the set of assume constraints accumulated across the translation.

assumes() - Method in class forge.translate.SymbolicExecutor

atom(int) - Method in class forge.util.RelationFactory

Returns the ith atom in the universe.

atoms() - Method in interface forge.solve.ForgeConstant.Tuple

B

baseMap() - Method in class forge.util.ModifiableMap

The unmodifiable base map.

BatchTransformer - Class in forge.transform

Applies a list of transformers in a row.

BatchTransformer(List<Transformer>) - Constructor for class forge.transform.BatchTransformer

BinaryExpression - Class in forge.program

An expression composed of a binary operator and two subexpressions.

BinaryExpression.Op - Enum in forge.program

Binding - Class in forge.solve

Binds variables to constants.

Binding(ForgeBounds) - Constructor for class forge.solve.Binding

Constructs an empty binding.

bitAnd(ForgeExpression) - Method in interface forge.program.ForgeExpression

bitNot() - Method in interface forge.program.ForgeExpression

bitOr(ForgeExpression) - Method in interface forge.program.ForgeExpression

bitWidth() - Method in class forge.solve.ForgeBounds

Return the bitwidth of integers in this bound.

bitXor(ForgeExpression) - Method in interface forge.program.ForgeExpression

bool() - Method in interface forge.program.ForgeExpression

bool() - Method in class forge.solve.BooleanAtom

bool() - Method in class forge.solve.InstanceAtom

bool() - Method in class forge.solve.IntegerAtom

boolAtom(boolean) - Method in class forge.solve.ForgeBounds

Return the boolean atom with the given value.

BooleanAtom - Class in forge.solve

A constant boolean expression: true or false.

BooleanDomain - Class in forge.program

Class of booleans.

booleanDomain() - Method in class forge.program.ForgeProgram

Returns the boolean domain.

BooleanLiteral - Class in forge.program

A constant boolean expression: true or false.

boolRelation() - Method in class forge.translate.RelationalModel

bound() - Method in class forge.solve.Binding

Returns an unmodifiable view of the set of bound modifiables.

boundInitial(ForgeVariable, ForgeConstant, ForgeConstant) - Method in class forge.solve.ForgeBounds

Bounds the initial value of the given variable anove and below.

bounds() - Method in class forge.solve.Binding

Returns the bounds to which this binding belongs.

BranchData<D> - Class in forge.dataflow

Output data from a transfer function on a branch stmt in dataflow analysis.

BranchData(D, D) - Constructor for class forge.dataflow.BranchData

Constructs a new branch data with the specified then and else data.

BranchData(D) - Constructor for class forge.dataflow.BranchData

Constructs a branch data where the then and else data are the same.

BranchStmt - Class in forge.cfg

A branching node of a Forge control flow graph.

BreadthFirstVisitor - Class in forge.util

Performs a breadth-first traversal of the call graph and then the statements within the call graph.

BreadthFirstVisitor() - Constructor for class forge.util.BreadthFirstVisitor

bringToPostState(ForgeExpression) - Static method in class forge.util.ExpressionUtil

Replace old expressions with variables under it.

bringToPreState(ForgeExpression) - Static method in class forge.util.ExpressionUtil

Replace all global variables with old expressions on these global variables.

bucket - Static variable in class forge.tests.CreateTest

build() - Method in class forge.solve.SolveOptions.Builder

Builds the SolveOptions.

buildingAnalysis() - Method in class forge.solve.ForgeReporter

Reports that Forge is building an analysis from a given specification and bounds.

buildingAnalysis() - Method in class forge.util.SystemOutReporter

C

called() - Method in class forge.cfg.CallStmt

CallStmt - Class in forge.cfg

A CFG node at which a procedure is called.

canProve() - Method in enum forge.solve.SolveOptions.SatSolver

Returns true if solver can provide a proof.

cfg() - Method in interface forge.cfg.CFGElement

Returns the cfg to which this element belongs.

cfg() - Method in class forge.cfg.CFGStmt

cfg() - Method in class forge.cfg.StmtSet

cfg() - Method in class forge.solve.Step

cfg() - Method in class forge.solve.Trace

CFGElement - Interface in forge.cfg

Belongs to a CFG.

CFGStmt - Class in forge.cfg

A stmt in a Forge control flow graph.

CFGVisitor - Interface in forge.cfg

A visitor to a stmt in a CFG.

check(ForgeCFG.Spec, ForgeBounds) - Method in class forge.solve.ForgeSolver

Finds a trace of the procedure within the given bounds that does not refine the given specification statement, determining coverage information in the case where no trace can be found if coverage flag is set to true.

checkAll(ForgeCFG.Spec, ForgeBounds) - Method in class forge.solve.ForgeSolver

checkAllTest() - Method in class forge.tests.ForgeTest

checkCFG(CFGElement) - Method in class forge.cfg.ForgeCFG

checkProgram(ProgramElement) - Method in class forge.program.ForgeProgram

checkSpec() - Method in class forge.tests.ForgeTest

checkTest() - Method in class forge.tests.ForgeTest

CircuitReporter - Class in forge.util

A reporter that prints the final circuit in eDIMACS form to a given file.

CircuitReporter(File) - Constructor for class forge.util.CircuitReporter

Constructs a new circuit reporter whose #translatingToCNF(kodkod.engine.bool.BooleanFormula) method will dump its argument to the given file, in eDIMACS format.

clear() - Method in class forge.cfg.StmtSet

closure() - Method in interface forge.program.ForgeExpression

closureTupleSet(BooleanMatrix) - Method in class forge.util.RelationFactory

Returns TupleSet that is the closure of a matrix.

code() - Method in class forge.solve.Coverage

code() - Method in class forge.solve.ForgeSolution

code() - Method in class forge.solve.ForgeSolver

code() - Method in class forge.tests.ForgeTest

columns() - Method in class forge.program.ProjectionExpression

compose(BinaryExpression.Op, ForgeExpression) - Method in interface forge.program.ForgeExpression

comprehension(LocalDecls) - Method in interface forge.program.ForgeExpression

cond() - Method in class forge.translate.SymbolicExecutor.BranchHook

condition() - Method in class forge.cfg.BranchStmt

condition() - Method in class forge.cfg.SpecStmt

condition() - Method in class forge.program.ConditionalExpression

ConditionalExpression - Class in forge.program

A conditional "if" expression

CONSTRAIN_STRATEGY - Static variable in class forge.tests.ForgeTest

ConstrainStrategy - Class in forge.translate

A translator strategy that introduces constraints wherever possible in lieu of inlining expressions.

contains(Object) - Method in class forge.cfg.StmtSet

containsAll(Collection<?>) - Method in class forge.cfg.StmtSet

copy(D) - Method in class forge.dataflow.DataflowAnalysis

Makes a copy of the specified data.

copy(Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

copy(Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

copy(Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

copy() - Method in class forge.solve.Binding

Constructs a copy of the specified binding.

copy(AssignStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

copy(CallStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

copy(CreateStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

copy(BranchStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

copy(SpecStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

copy() - Method in class forge.translate.Environment

CopyTreeTest - Class in forge.tests

Coverage - Class in forge.solve

Coverage of a

coverage() - Method in class forge.solve.ForgeSolution

Return the statements covered by the analysis if unsatisfiable; otherwise null.

coverage(boolean) - Method in class forge.solve.SolveOptions.Builder

Chooses whether solver measures coverage.

coverage() - Method in class forge.solve.SolveOptions

Returns whether coverage metric is on.

Coverage.Score - Class in forge.solve

A coverage score given to a statement.

CoverageTest - Class in forge.tests

Used to distinguish the coverage offered by the three different translation strategies.

CoverageTest() - Constructor for class forge.tests.CoverageTest

createRelation() - Method in class forge.translate.RelationalModel.DomainRelations

CreateStmt - Class in forge.cfg

A stmt which constructs a new instance of a class and assigns that instance to a local variable.

CreateTest - Class in forge.tests

CreateTest() - Constructor for class forge.tests.CreateTest

currOptions() - Method in class forge.tests.ForgeTest

D

dataAfter(UpdateStmt) - Method in class forge.dataflow.AnalysisResults

Returns the data at the program point in the CFG immediately following the specified update stmt.

dataAfter(BranchStmt) - Method in class forge.dataflow.AnalysisResults

Returns the data at the program points in the CFG that immediately follow the specified branch stmt.

dataBefore(CFGStmt) - Method in class forge.dataflow.AnalysisResults

Returns the data at the program point in the CFG immediately preceding the specified stmt.

DataflowAnalysis<D> - Class in forge.dataflow

A template for a dataflow analysis.

DataflowAnalysis(boolean) - Constructor for class forge.dataflow.DataflowAnalysis

Constructs a new dataflow analysis in the specified direction.

decls() - Method in class forge.program.QuantifyExpression

defaultVisit(ForgeExpression) - Method in class forge.transform.ExpressionDefaulter

defaultVisit(CFGStmt) - Method in class forge.util.BreadthFirstVisitor

descend(BinaryExpression) - Method in class forge.transform.ExpressionDescender

Applies visitor to left and right subexpression.

descend(UnaryExpression) - Method in class forge.transform.ExpressionDescender

Applies visitor to subexpression.

descend(QuantifyExpression) - Method in class forge.transform.ExpressionDescender

Applies visitor to variable and subexpression.

descend(ConditionalExpression) - Method in class forge.transform.ExpressionDescender

Applies visitor to condition, then, and else expressions.

descend(ProjectionExpression) - Method in class forge.transform.ExpressionDescender

Applies visitor to subexpression

descend(OldExpression) - Method in class forge.transform.ExpressionDescender

Applies visitor to variable.

descend(ForgeVariable) - Method in class forge.transform.ExpressionDescender

Does nothing.

descend(ForgeLiteral) - Method in class forge.transform.ExpressionDescender

Does nothing.

descend(ForgeType) - Method in class forge.transform.ExpressionDescender

Does nothing.

detectedSymmetries(Set<?>) - Method in class forge.solve.ForgeReporter

Reports the symmetries detected by Kodkod as a set of (kodkod.util.ints.IntSet) objects.

detectedSymmetries(Set<?>) - Method in class forge.util.SystemOutReporter

detectingSymmetries(Object) - Method in class forge.solve.ForgeReporter

Reports that Kodkod is detecting symmetries in the given bounds (kodkod.instance.Bounds).

detectingSymmetries(Object) - Method in class forge.util.SystemOutReporter

difference(ForgeExpression) - Method in interface forge.program.ForgeExpression

difference(ForgeType) - Method in interface forge.program.ForgeType

difference(ForgeType) - Method in interface forge.program.ForgeType.Unary

difference(ForgeConstant) - Method in interface forge.solve.ForgeConstant

difference(ForgeConstant) - Method in interface forge.solve.ForgeConstant.Unary

differenceTupleSet(BooleanMatrix, BooleanMatrix) - Method in class forge.util.RelationFactory

Returns TupleSet that is the difference of two matrices.

diffMap() - Method in class forge.util.ModifiableMap

The modifiable diff map.

divide(ForgeExpression) - Method in interface forge.program.ForgeExpression

domain() - Method in interface forge.program.ForgeExpression

domain() - Method in interface forge.program.ForgeType

domain() - Method in interface forge.program.ForgeType.Tuple

domain() - Method in interface forge.solve.ForgeConstant

domain() - Method in interface forge.solve.ForgeConstant.Tuple

domainRelations(InstanceDomain) - Method in class forge.translate.RelationalModel

domains() - Method in interface forge.program.ForgeType.Tuple

DominatorAnalysis - Class in forge.dataflow

Computes the dominators for each node in the CFG.

E

elseData() - Method in class forge.dataflow.BranchData

Returns the else data.

elseExpr() - Method in class forge.program.ConditionalExpression

empty(ForgeCFG) - Static method in class forge.cfg.StmtSet

empty() - Method in class forge.program.ForgeProgram

Returns the empty set constant/type.

empty(int) - Method in class forge.program.ForgeProgram

Returns the empty constant/type of the specified arity.

empty() - Method in class forge.solve.ForgeBounds

Return the empty unary constant.

empty(int) - Method in class forge.solve.ForgeBounds

Return the empty constant of the given arity.

empty() - Method in class forge.util.RelationFactory

Returns the empty set relation.

empty(int) - Method in class forge.util.RelationFactory

Returns the empty relation of the given arity.

emptyDecls() - Method in class forge.program.ForgeProgram

Returns the empty decls.

emptyTupleSet(int) - Method in class forge.util.RelationFactory

Returns an empty TupleSet of the given arity.

entry() - Method in class forge.cfg.ForgeCFG

Returns the entry stmt of the cfg.

entry() - Method in class forge.cfg.ForgeCFG.Impl

entry() - Method in class forge.cfg.ForgeCFG.Spec

env() - Method in class forge.translate.ExprTranslator

Environment - Class in forge.translate

Symbolic execution environment maintained by the translation.

Environment(RelationalModel) - Constructor for class forge.translate.Environment

eq(ForgeExpression) - Method in interface forge.program.ForgeExpression

equals(Object) - Method in class forge.cfg.StmtSet

equals(Object) - Method in class forge.solve.Coverage.Score

evaluate(ForgeExpression) - Method in class forge.solve.Trace

evaluateBool(ForgeExpression) - Method in class forge.solve.Trace

evaluateInt(ForgeExpression) - Method in class forge.solve.Trace

execute(SymbolicExecutor.AssignHook) - Method in class forge.translate.ConstrainStrategy

execute(SymbolicExecutor.CreateHook) - Method in class forge.translate.ConstrainStrategy

execute(SymbolicExecutor.SpecHook) - Method in class forge.translate.ConstrainStrategy

execute(SymbolicExecutor.AssignHook) - Method in class forge.translate.HybridStrategy

execute(SymbolicExecutor.CreateHook) - Method in class forge.translate.HybridStrategy

execute(SymbolicExecutor.SpecHook) - Method in class forge.translate.HybridStrategy

execute(SymbolicExecutor.AssignHook) - Method in class forge.translate.InlineStrategy

execute(SymbolicExecutor.CreateHook) - Method in class forge.translate.InlineStrategy

execute(SymbolicExecutor.SpecHook) - Method in class forge.translate.InlineStrategy

execute(SymbolicExecutor.AssignHook) - Method in interface forge.translate.SEStrategy

execute(SymbolicExecutor.CreateHook) - Method in interface forge.translate.SEStrategy

execute(SymbolicExecutor.SpecHook) - Method in interface forge.translate.SEStrategy

execute(AssignStmt) - Method in class forge.translate.SymbolicExecutor

execute(CreateStmt) - Method in class forge.translate.SymbolicExecutor

execute(SpecStmt) - Method in class forge.translate.SymbolicExecutor

execute(SymbolicExecutor.AssignHook) - Method in class forge.translate.ThesisStrategy

execute(SymbolicExecutor.CreateHook) - Method in class forge.translate.ThesisStrategy

execute(SymbolicExecutor.SpecHook) - Method in class forge.translate.ThesisStrategy

exit() - Method in class forge.cfg.ForgeCFG

Returns the exit stmt of the cfg.

exitData() - Method in class forge.dataflow.AnalysisResults

Returns the data at the program point in the CFG immediately following the exit node.

ExitStmt - Class in forge.cfg

A terminal stmt of a control flow graph.

explicitExpr(ForgeVariable) - Method in class forge.cfg.SpecStmt

Returns a functional expression for the given modified variable, or null if the variable is not constrained in a functional way.

expr() - Method in class forge.cfg.AssignStmt

ExpressionDefaulter<T> - Class in forge.transform

Visitor where each visit method calls the default method.

ExpressionDefaulter() - Constructor for class forge.transform.ExpressionDefaulter

ExpressionDescender - Class in forge.transform

Descends through a Forge expression graph without caching.

ExpressionDescender() - Constructor for class forge.transform.ExpressionDescender

ExpressionReplacer - Class in forge.transform

A depth-first visitor that replaces each node in the expression.

ExpressionReplacer() - Constructor for class forge.transform.ExpressionReplacer

ExpressionUtil - Class in forge.util

Utilities with expressions.

ExpressionVisitor<T> - Class in forge.program

A visitor to a Forge expression.

ExpressionVisitor() - Constructor for class forge.program.ExpressionVisitor

ExpressionVisitor(ExpressionVisitor<T>) - Constructor for class forge.program.ExpressionVisitor

ExprTranslator - Class in forge.translate

Translates Forge expressions into Kodkod expressions.

ExprTranslator(Environment) - Constructor for class forge.translate.ExprTranslator

extent(ForgeDomain) - Method in class forge.solve.ForgeBounds

Return the extent of the given domain type.

extent(ForgeType.Unary) - Method in class forge.solve.ForgeBounds

Return the extent of the given unary type.

extent(ForgeType.Tuple) - Method in class forge.solve.ForgeBounds

Return the extent of the given tuple type.

extent(ForgeType) - Method in class forge.solve.ForgeBounds

Return the extent of the given type.

extentExpr() - Method in class forge.translate.RelationalModel.DomainRelations

F

falseLiteral() - Method in class forge.program.ForgeProgram

Returns the false literal.

falseRelation() - Method in class forge.translate.RelationalModel

finalBind() - Method in class forge.solve.Trace

finalEnv() - Method in class forge.translate.ForgeTranslation

Returns the final environment.

findModifiables(ForgeExpression) - Static method in class forge.util.ExpressionUtil

Returns the set of variables found in the given expression, provided the expression does not contain any old expressions.

firstRelation() - Method in class forge.translate.RelationalModel.DomainRelations

flatten(ForgeExpression) - Static method in class forge.util.ExpressionUtil

Flattens conjunctions into a set of top-level constraints.

flattening(Object) - Method in class forge.solve.ForgeReporter

Reports that Kodkod flattering of the given boolean circuit (kodkod.engine.bool.BooleanFormula) is in progress.

flattening(Object) - Method in class forge.util.SystemOutReporter

forAll(LocalDecls) - Method in interface forge.program.ForgeExpression

forge.cfg - package forge.cfg

forge.dataflow - package forge.dataflow

forge.program - package forge.program

forge.solve - package forge.solve

forge.tests - package forge.tests

forge.transform - package forge.transform

forge.translate - package forge.translate

forge.util - package forge.util

ForgeAtom - Class in forge.solve

A singleton constant

ForgeBounds - Class in forge.solve

Bounds type and the intial value of variables by constants.

ForgeBounds(ForgeProgram, int, Map<InstanceDomain, Integer>) - Constructor for class forge.solve.ForgeBounds

ForgeCFG - Class in forge.cfg

The CFG of a procedure.

ForgeCFG.Impl - Class in forge.cfg

An implementation CFG with several statements.

ForgeCFG.Spec - Class in forge.cfg

A specification CFG containing only a single specification statement.

ForgeConstant - Interface in forge.solve

A Forge constant -- a relation of atoms.

ForgeConstant.Tuple - Interface in forge.solve

A constant that is a tuple of atoms.

ForgeConstant.Unary - Interface in forge.solve

A constant that is a set of atoms.

ForgeDomain - Class in forge.program

A set of atoms disjoint from all other classes.

ForgeDomain.Kind - Enum in forge.program

ForgeExpression - Interface in forge.program

A Forge expression.

ForgeExpression.Leaf - Interface in forge.program

Domains, variables, and literals -- expressions that have a name.

ForgeExpression.Modifiable - Interface in forge.program

Variables and instance domains -- leafs that may be modified.

ForgeLiteral - Class in forge.program

A singleton constant

ForgeProcedure - Class in forge.program

A procedure in a Forge program.

ForgeProgram - Class in forge.program

Manages the Forge classes, fields, and procedures.

ForgeProgram() - Constructor for class forge.program.ForgeProgram

Constructs an empty Forge program.

ForgeReporter - Class in forge.solve

Reports details of the Forge and underlying Kodkod analysis.

ForgeReporter() - Constructor for class forge.solve.ForgeReporter

ForgeSolution - Class in forge.solve

A solution that includes coverage information when it is unsatisfiable.

ForgeSolver - Class in forge.solve

Binds instance literals to atoms.

ForgeSolver(ForgeCFG, int) - Constructor for class forge.solve.ForgeSolver

Constructs a solver for analyzing the given code, where loops and recursion are unrolled the specified number of times.

ForgeSolver(ForgeCFG, SolveOptions) - Constructor for class forge.solve.ForgeSolver

Constructs a solver for analyzing the given code with the given options.

ForgeTest - Class in forge.tests

A generic Forge Test to be extended

ForgeTest(String, ForgeCFG, ForgeExpression, ForgeExpression, Set<GlobalVariable>) - Constructor for class forge.tests.ForgeTest

ForgeTranslation - Class in forge.translate

A translation of a Forge procedure to Kodkod.

ForgeType - Interface in forge.program

The type of a Forge expression.

ForgeType.Tuple - Interface in forge.program

A type that is a tuple of classes.

ForgeType.Unary - Interface in forge.program

A type that is a set of classes.

ForgeVariable - Class in forge.program

A global or local Forge variable.

forSome(LocalDecls) - Method in interface forge.program.ForgeExpression

G

generalSpecification(ForgeProcedure, Set<? extends ForgeVariable>, ForgeExpression) - Static method in class forge.cfg.ForgeCFG

Returns a new unmodifiable CFG that who entry is a specification stmt with the given set of modifiables.

generatingSBP() - Method in class forge.solve.ForgeReporter

Reports that Kodkod SBP is in progress.

generatingSBP() - Method in class forge.util.SystemOutReporter

getCache(ForgeExpression) - Method in class forge.program.ExpressionVisitor

getElse() - Method in class forge.cfg.BranchStmt

getExpr(ForgeExpression.Modifiable) - Method in class forge.translate.Environment

Gets the expression for the given modifiable.

getNext() - Method in class forge.cfg.UpdateStmt

getThen() - Method in class forge.cfg.BranchStmt

getValue(ForgeExpression.Modifiable) - Method in class forge.solve.Binding

Returns the constant to which the given modifiable is bound.

globalRelation(GlobalVariable) - Method in class forge.translate.RelationalModel

GlobalVariable - Class in forge.program

A relation over Forge classes.

globalVariables() - Method in class forge.program.ForgeProgram

Returns the set of all global variables in the program.

gt(ForgeExpression) - Method in interface forge.program.ForgeExpression

gte(ForgeExpression) - Method in interface forge.program.ForgeExpression

H

hash(ForgeCFG) - Static method in class forge.cfg.StmtSet

hash(StmtSet) - Static method in class forge.cfg.StmtSet

hashCode() - Method in class forge.cfg.StmtSet

hashCode() - Method in class forge.solve.Coverage.Score

HYBRID_STRATEGY - Static variable in class forge.tests.ForgeTest

HybridStrategy - Class in forge.translate

A translator that inlines for updates but adds constraints for branches

I

id() - Method in class forge.cfg.CFGStmt

Returns a unique id for this stmt.

iden() - Method in interface forge.program.ForgeExpression

IDENTITY - Static variable in interface forge.transform.Transformer

The identity transformer.

iff(ForgeExpression) - Method in interface forge.program.ForgeExpression

IllegalArityException - Exception in forge.program

Thrown when an expression is constructed from illegal arities.

implementation(ForgeProcedure) - Static method in class forge.cfg.ForgeCFG

Returns a new modifiable CFG that who entry is the exit stmt.

implies(ForgeExpression) - Method in interface forge.program.ForgeExpression

in(ForgeExpression) - Method in interface forge.program.ForgeExpression

inArgs() - Method in class forge.cfg.CallStmt

initial() - Method in class forge.dataflow.DataflowAnalysis

Returns the initial data set.

initial() - Method in class forge.dataflow.DominatorAnalysis

initial() - Method in class forge.dataflow.InverseDominatorAnalysis

initial() - Method in class forge.dataflow.ReachabilityAnalysis

initialBind() - Method in class forge.solve.Trace

initialEnv() - Method in class forge.translate.ForgeTranslation

Returns the initial environment.

initialize(SEStrategy, ForgeCFG, boolean) - Static method in class forge.translate.SymbolicExecutor

initialLowerBound(ForgeVariable) - Method in class forge.solve.ForgeBounds

Return the initial lower bound for the given variable.

initialRelation() - Method in class forge.translate.RelationalModel.DomainRelations

initialUpperBound(ForgeVariable) - Method in class forge.solve.ForgeBounds

Return the initial upper bound for the given variable.

INLINE_STRATEGY - Static variable in class forge.tests.ForgeTest

InlineStrategy - Class in forge.translate

A translator strategy that inlines expressions wherever possible in lieu of introducing constraints.

InlineTransformer - Class in forge.transform

Inlines all the calls in a call graph into a procedure.

InlineTransformer(int) - Constructor for class forge.transform.InlineTransformer

Constructs a call inliner that unrolls recursion the given number of times.

inParams() - Method in class forge.program.ForgeProcedure

Returns the set of in-parameters.

instanceAtom(InstanceDomain, int) - Method in class forge.solve.ForgeBounds

Return the ith atom allocated for the given instance domain.

instanceAtom(InstanceLiteral) - Method in class forge.solve.ForgeBounds

Return the atom allocated for the given instance literal.

InstanceAtom - Class in forge.solve

An atom in an Atom class.

instanceBound(InstanceDomain) - Method in class forge.solve.ForgeBounds

Return the number of atoms to which the given domain is limited.

InstanceDomain - Class in forge.program

A class of instance (non-primitive) atoms.

instanceDomains() - Method in class forge.program.ForgeProgram

Returns the instance domains.

InstanceLiteral - Class in forge.program

An atom in an Atom class.

instanceLiterals() - Method in class forge.program.ForgeProgram

Returns the set of all instance literals.

intAtom(int) - Method in class forge.solve.ForgeBounds

Return integer atom with the given value.

intConstant(IntegerLiteral) - Method in class forge.translate.RelationalModel

IntegerAtom - Class in forge.solve

A constant boolean expression: true or false.

integerDomain() - Method in class forge.program.ForgeProgram

Returns the integer domain.

IntegerDomain - Class in forge.program

Class of integers.

integerLiteral(int) - Method in class forge.program.ForgeProgram

Returns the integer literal with the specified value.

IntegerLiteral - Class in forge.program

A constant integer expression.

intersection(ForgeExpression) - Method in interface forge.program.ForgeExpression

intersection(ForgeType) - Method in interface forge.program.ForgeType

intersection(ForgeType) - Method in interface forge.program.ForgeType.Unary

intersection(ForgeConstant) - Method in interface forge.solve.ForgeConstant

intersection(ForgeConstant) - Method in interface forge.solve.ForgeConstant.Unary

intersectTupleSet(BooleanMatrix, BooleanMatrix) - Method in class forge.util.RelationFactory

Returns TupleSet that is the intersection of two matrices.

intRelation() - Method in class forge.translate.RelationalModel

InverseDominatorAnalysis - Class in forge.dataflow

Computes the inverse dominators for each node in the CFG.

isBackward() - Method in class forge.dataflow.DataflowAnalysis

Returns true if this is a backwards analysis.

isBranch() - Method in class forge.solve.Step.Branch

isBranch() - Method in class forge.solve.Step

isBranch() - Method in class forge.solve.Step.Update

isCached(ForgeExpression) - Method in class forge.program.ExpressionVisitor

isCall() - Method in class forge.solve.Step.Call

isCall() - Method in class forge.solve.Step.Update

isDomain() - Method in interface forge.program.ForgeType

isEmpty() - Method in class forge.cfg.StmtSet

isEmpty() - Method in interface forge.program.ForgeType

isEmpty() - Method in interface forge.solve.ForgeConstant

Returns if the size is 0.

isFunction() - Method in class forge.program.ProjectionExpression

isGlobal() - Method in interface forge.program.ForgeExpression.Modifiable

True if instanceof InstanceDomain or GlobalVariable, false if LocalVariable.

isGlobal() - Method in class forge.program.GlobalVariable

isGlobal() - Method in class forge.program.InstanceDomain

isGlobal() - Method in class forge.program.LocalVariable

isTuple() - Method in interface forge.solve.ForgeConstant

Returns true if the size is one.

isUnary() - Method in interface forge.program.ForgeExpression

Returns true if the arity is one.

isUnary() - Method in interface forge.solve.ForgeConstant

Returns true if the arity is one.

isVariable() - Method in interface forge.program.ForgeExpression.Modifiable

True if instanceof ForgeVariable, false if InstanceDomain.

isVariable() - Method in class forge.program.ForgeVariable

isVariable() - Method in class forge.program.InstanceDomain

iterator() - Method in class forge.cfg.StmtSet

iterator() - Method in class forge.translate.RelationalModel.StmtRelations

J

join(ForgeExpression) - Method in interface forge.program.ForgeExpression

join(ForgeType) - Method in interface forge.program.ForgeType

join(ForgeConstant) - Method in interface forge.solve.ForgeConstant

joinTupleSet(BooleanMatrix, BooleanMatrix) - Method in class forge.util.RelationFactory

Returns TupleSet that is the join of two matrices.

K

kind() - Method in class forge.program.ForgeDomain

kkCore() - Method in class forge.solve.Coverage

Returns set of Kodkod formulas in the core.

kkFormula() - Method in class forge.solve.ForgeSolution

Returns set of Kodkod formula solved.

kkInstance() - Method in class forge.solve.Trace

Returns the Kodkod instance from which this trace was created.

L

left() - Method in class forge.program.BinaryExpression

listDomain() - Method in class forge.tests.ListTest

listOfAtoms(TupleSet) - Method in class forge.util.RelationFactory

Wraps the given singleton TupleSet as a list of atoms.

ListTest - Class in forge.tests

Constructs a FIR program consisting of a list data structure and two implementations of the contains method, one that contains a loop and the other that contains a recursive call.

ListTest.Looping - Class in forge.tests

ListTest.Looping() - Constructor for class forge.tests.ListTest.Looping

ListTest.Recursive - Class in forge.tests

ListTest.Recursive() - Constructor for class forge.tests.ListTest.Recursive

literalRelation(InstanceLiteral) - Method in class forge.translate.RelationalModel

literalsExpr() - Method in class forge.translate.RelationalModel.DomainRelations

LocalDecls - Interface in forge.program

Interface to an ordered set of local variables

LocalDecls.EmptyDecls - Class in forge.program

An empty set of decls.

LocalDecls.MultiDecls - Class in forge.program

A set of one or more local variables.

locals() - Method in class forge.program.LocalDecls.EmptyDecls

locals() - Method in interface forge.program.LocalDecls

Returns the local variables in this decls.

locals() - Method in class forge.program.LocalDecls.MultiDecls

locals() - Method in class forge.program.LocalVariable

LocalVariable - Class in forge.program

A Forge local variable.

lone() - Method in interface forge.program.ForgeExpression

lt(ForgeExpression) - Method in interface forge.program.ForgeExpression

lte(ForgeExpression) - Method in interface forge.program.ForgeExpression

M

main(String[]) - Static method in class forge.tests.CoverageTest

main(String[]) - Static method in class forge.tests.CreateTest

main(String[]) - Static method in class forge.tests.ListTest

Constructs the FIR and checks both of the contains procedures for any counterexamples within the bounds described above.

main(String[]) - Static method in class forge.tests.MultiplyTest

main(String[]) - Static method in class forge.tests.RegisterTest

main(String[]) - Static method in class forge.tests.StrategyComparison

main(String[]) - Static method in class forge.tests.TopologicalSortTest

main(String[]) - Static method in class forge.tests.TreeIntSetTest

main(String[]) - Static method in class forge.tests.TreeIntSetTest2

main(String[]) - Static method in class forge.tests.ZuneTest

make(TupleSet) - Method in class forge.util.RelationFactory

Makes a relation from a TupleSet.

makeBounds() - Method in class forge.util.RelationFactory

Returns a new bounds object with the universe.

makeTuple(TupleSet) - Method in class forge.util.RelationFactory

Makes a tuple relation from a TupleSet.

makeUnary(TupleSet) - Method in class forge.util.RelationFactory

Makes a unary relation from a TupleSet.

maxIntValue() - Method in class forge.solve.ForgeBounds

Return the maximum integer allowed by the bitwidth.

merge(D, D) - Method in class forge.dataflow.DataflowAnalysis

Merges "from" data into the "into" data and return true iff the into data has changed.

merge(Set<CFGStmt>, Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

merge(Set<CFGStmt>, Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

merge(Set<CFGStmt>, Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

merge(SymbolicExecutor.BranchHook, ForgeExpression.Modifiable, Expression, Expression) - Method in class forge.translate.ConstrainStrategy

merge(SymbolicExecutor.BranchHook, ForgeExpression.Modifiable, Expression, Expression) - Method in class forge.translate.HybridStrategy

merge(SymbolicExecutor.BranchHook, ForgeExpression.Modifiable, Expression, Expression) - Method in class forge.translate.InlineStrategy

merge(SymbolicExecutor.BranchHook, ForgeExpression.Modifiable, Expression, Expression) - Method in interface forge.translate.SEStrategy

merge(BranchStmt, SymbolicExecutor, SymbolicExecutor) - Method in class forge.translate.SymbolicExecutor

Merge symbolic execution from both sides of a branch.

merge(SymbolicExecutor.BranchHook, ForgeExpression.Modifiable, Expression, Expression) - Method in class forge.translate.ThesisStrategy

minIntValue() - Method in class forge.solve.ForgeBounds

Return the minimum integer allowed by the bitwidth.

minus(ForgeExpression) - Method in interface forge.program.ForgeExpression

model() - Method in class forge.translate.Environment

model() - Method in class forge.translate.ExprTranslator

model() - Method in class forge.translate.ForgeTranslation

ModifiableMap<V> - Class in forge.util

An override map that maps modifiables to non-null values.

ModifiableMap() - Constructor for class forge.util.ModifiableMap

ModifiableMap(Map<ForgeExpression.Modifiable, V>) - Constructor for class forge.util.ModifiableMap

modified() - Method in class forge.cfg.AssignStmt

modified() - Method in class forge.cfg.CallStmt

modified() - Method in class forge.cfg.CreateStmt

modified() - Method in class forge.cfg.SpecStmt

modified() - Method in class forge.cfg.UpdateStmt

Returns the set of variables and instance domains that may be modified by the statement.

mods() - Method in class forge.translate.Environment

Returns the set of all modifiables in the environment.

modulo(ForgeExpression) - Method in interface forge.program.ForgeExpression

MultiplyTest - Class in forge.tests

Good for testing nested loop unrolling.

MultiplyTest() - Constructor for class forge.tests.MultiplyTest

N

name() - Method in class forge.program.ForgeDomain

name() - Method in interface forge.program.ForgeExpression.Leaf

Returns the expression's name.

name() - Method in class forge.program.ForgeLiteral

name() - Method in class forge.program.ForgeProcedure

Returns the name of the procedure.

name() - Method in class forge.program.ForgeVariable

name() - Method in class forge.solve.ForgeAtom

name() - Method in class forge.tests.ForgeTest

neg() - Method in interface forge.program.ForgeExpression

newAssign(ForgeVariable, ForgeExpression) - Method in class forge.cfg.ForgeCFG.Impl

Constructs a new assign stmt with the specified variable and expr, whose successor is the exit stmt of this cfg.

newAssume(ForgeExpression) - Method in class forge.cfg.ForgeCFG.Impl

Constructs a new spec stmt with the specified condition and no modified variables, whose successor is the exit stmt of this cfg.

newBig(TupleSet) - Method in class forge.util.RelationFactory

Constructs a new instance of a TupleSet with a size > 1 and arity > 1.

newBranch(ForgeExpression) - Method in class forge.cfg.ForgeCFG.Impl

Constructs a new branch node with the specified condition value, whose successors are both the exit stmt of this cfg.

newCall(ForgeCFG, List<ForgeExpression>, List<ForgeVariable>) - Method in class forge.cfg.ForgeCFG.Impl

Constructs a new call stmt with the specified values, whose successor is the exit stmt of this cfg.

newCreate(ForgeVariable, InstanceDomain) - Method in class forge.cfg.ForgeCFG.Impl

Constructs a new create stmt with the specified values, whose successor is the exit stmt of this cfg.

newGlobalVariable(String, ForgeType) - Method in class forge.program.ForgeProgram

Constructs and returns a new global variable.

newInstanceDomain(String) - Method in class forge.program.ForgeProgram

Constructs and returns a new instance domain.

newInstanceLiteral(String, InstanceDomain) - Method in class forge.program.ForgeProgram

Constructs and returns a new instance literal.

newLocalVariable(String, ForgeType) - Method in class forge.program.ForgeProgram

Constructs and returns a new local variable.

newOptions(int) - Method in class forge.tests.ForgeTest

newProcedure(String, LocalDecls, LocalDecls) - Method in class forge.program.ForgeProgram

Constructs and returns a new procedure.

newSpec(Set<? extends ForgeVariable>, ForgeExpression) - Method in class forge.cfg.ForgeCFG.Impl

Constructs a new assume stmt with the specified condition and the given set of modified variables, whose successor is the exit stmt of this cfg.

newTuple(TupleSet) - Method in class forge.util.RelationFactory

Constructs a new instance of a TupleSet with a size > 1 and arity = 1.

newUnary(TupleSet) - Method in class forge.util.RelationFactory

Constructs a new instance of a TupleSet with a size = 1 and arity > 1.

no() - Method in interface forge.program.ForgeExpression

NO_GLOBALS - Static variable in class forge.tests.ForgeTest

NO_SCOPES - Static variable in class forge.tests.ForgeTest

nodeDomain() - Method in class forge.tests.TreeIntSetTest

nodeDomain() - Method in class forge.tests.TreeIntSetTest2

not() - Method in interface forge.program.ForgeExpression

notCond() - Method in class forge.translate.SymbolicExecutor.BranchHook

O

old() - Method in class forge.program.ForgeVariable

OldExpression - Class in forge.program

Refers to the old value of a modified variable in an assume statement.

one() - Method in interface forge.program.ForgeExpression

op() - Method in class forge.program.BinaryExpression

op() - Method in class forge.program.QuantifyExpression

op() - Method in class forge.program.UnaryExpression

optimizingBoundsAndFormula() - Method in class forge.solve.ForgeReporter

Reports that Kodkod is optimizing the bounds and formula.

optimizingBoundsAndFormula() - Method in class forge.util.SystemOutReporter

options() - Method in class forge.solve.ForgeSolver

or(ForgeExpression) - Method in interface forge.program.ForgeExpression

orderRelation() - Method in class forge.translate.RelationalModel.DomainRelations

outArgs() - Method in class forge.cfg.CallStmt

outParams() - Method in class forge.program.ForgeProcedure

Returns the set of out-parameters.

override(ForgeExpression) - Method in interface forge.program.ForgeExpression

overrideTupleSet(BooleanMatrix, BooleanMatrix) - Method in class forge.util.RelationFactory

Returns TupleSet that is the override of two matrices.

P

paramRelation(LocalVariable) - Method in class forge.translate.RelationalModel

pinOldExpr(ForgeVariable) - Method in class forge.translate.ExprTranslator

Pins the old expression for the duration of the next translation.

plus(ForgeExpression) - Method in interface forge.program.ForgeExpression

post() - Method in class forge.solve.Step.Update

preds() - Method in class forge.cfg.CFGStmt

Returns an unmodifiable view of the predecessor stmts.

prettyPrint(ForgeExpression) - Static method in class forge.util.ExpressionUtil

Pretty-prints the given expression to the given PrintStream.

procedure() - Method in class forge.cfg.ForgeCFG

product(ForgeExpression) - Method in interface forge.program.ForgeExpression

product(ForgeType) - Method in interface forge.program.ForgeType

product(ForgeType.Tuple) - Method in interface forge.program.ForgeType.Tuple

product(ForgeConstant) - Method in interface forge.solve.ForgeConstant

product(ForgeConstant.Tuple) - Method in interface forge.solve.ForgeConstant.Tuple

program() - Method in class forge.cfg.CFGStmt

program() - Method in class forge.cfg.ForgeCFG

program() - Method in class forge.cfg.StmtSet

program() - Method in class forge.program.ForgeProcedure

program() - Method in class forge.program.LocalDecls.EmptyDecls

program() - Method in class forge.program.LocalDecls.MultiDecls

program() - Method in interface forge.program.ProgramElement

Returns the program to which this element belongs.

program() - Method in class forge.solve.Binding

program() - Method in class forge.solve.ForgeBounds

program() - Method in class forge.solve.ForgeSolution

program() - Method in class forge.solve.ForgeSolver

program() - Method in class forge.solve.Step

program() - Method in class forge.solve.Trace

program() - Method in class forge.translate.Environment

program() - Method in class forge.translate.ExprTranslator

program() - Method in class forge.translate.ForgeTranslation

program() - Method in class forge.translate.RelationalModel

program() - Method in class forge.util.RelationFactory

ProgramElement - Interface in forge.program

Belongs to a program.

projection(int...) - Method in interface forge.program.ForgeExpression

projection(int...) - Method in interface forge.solve.ForgeConstant

projection(int...) - Method in interface forge.solve.ForgeConstant.Tuple

ProjectionExpression - Class in forge.program

An expression for a relational projection over another expression.

projectTupleSet(BooleanMatrix, int...) - Method in class forge.util.RelationFactory

Returns TupleSet that is the projection of a matrix over some columns.

projectType(int...) - Method in interface forge.program.ForgeType

projectType(int...) - Method in interface forge.program.ForgeType.Tuple

put(ForgeExpression.Modifiable, V) - Method in class forge.util.ModifiableMap

putCache(ForgeExpression, T) - Method in class forge.program.ExpressionVisitor

putExpr(ForgeExpression.Modifiable, Expression) - Method in class forge.translate.Environment

Sets the expression for the given modifiable.

putValue(ForgeExpression.Modifiable, ForgeConstant) - Method in class forge.solve.Binding

Maps the given modifiable to the given constant.

Q

quantify(QuantifyExpression.Op, LocalDecls) - Method in interface forge.program.ForgeExpression

QuantifyExpression - Class in forge.program

A quantified formula expression.

QuantifyExpression.Op - Enum in forge.program

R

range() - Method in interface forge.program.ForgeExpression

range() - Method in interface forge.program.ForgeType

range() - Method in interface forge.program.ForgeType.Tuple

range() - Method in interface forge.solve.ForgeConstant

range() - Method in interface forge.solve.ForgeConstant.Tuple

ReachabilityAnalysis - Class in forge.dataflow

Computes the set of nodes reachable from each node in the CFG (not including the node itself unless the node is part of a cycle).

referenced() - Method in class forge.cfg.AssignStmt

referenced() - Method in class forge.cfg.BranchStmt

referenced() - Method in class forge.cfg.CallStmt

referenced() - Method in class forge.cfg.CreateStmt

referenced() - Method in class forge.cfg.ReferenceStmt

Returns the set of variables and instance domains referenced by the statement.

referenced() - Method in class forge.cfg.SpecStmt

ReferenceStmt - Class in forge.cfg

A statement in the control-flow graph that may reference the current value of modifiables.

RegisterTest - Class in forge.tests

RegisterTest() - Constructor for class forge.tests.RegisterTest

RelationalModel - Class in forge.translate

Stores the relations for the translator.

RelationalModel.DomainRelations - Class in forge.translate

Relations created for an InstanceDomain.

RelationalModel.StmtRelations - Class in forge.translate

Relations created for a statement.

RelationFactory<R,U extends R,T extends R,A extends U,O> - Class in forge.util

Implementation support for factories that construct relations with Kodkod TupleSets.

RelationFactory(ForgeProgram) - Constructor for class forge.util.RelationFactory

remove(Object) - Method in class forge.cfg.StmtSet

removeAll(Collection<?>) - Method in class forge.cfg.StmtSet

replace(CFGStmt, CFGStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Sets the result of applying the visitor to the given source.

replaceDecls(LocalDecls) - Method in class forge.transform.ExpressionReplacer

replaceDom(InstanceDomain) - Method in class forge.transform.AbstractTransformer.TransformVisitor

replaceExpr(ForgeExpression) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Called during the copy methods on any expression that appears.

replaceExprs(List<ForgeExpression>) - Method in class forge.transform.AbstractTransformer.TransformVisitor

replaceVar(ForgeVariable) - Method in class forge.transform.AbstractTransformer.TransformVisitor

replaceVariable(ForgeExpression, ForgeVariable, ForgeVariable) - Static method in class forge.util.ExpressionUtil

Replace all occurrences of variable from to variable to.

replaceVariables(ForgeExpression, Map<ForgeVariable, ForgeVariable>) - Static method in class forge.util.ExpressionUtil

Replaces variables according to the map (map is from variables to be replaced to their desired replacements.)

replaceVars(Collection<ForgeVariable>) - Method in class forge.transform.AbstractTransformer.TransformVisitor

reporter(ForgeReporter) - Method in class forge.solve.SolveOptions.Builder

Chooses the reporter.

reporter() - Method in class forge.solve.SolveOptions

REPORTER - Static variable in class forge.util.SystemOutReporter

retainAll(Collection<?>) - Method in class forge.cfg.StmtSet

right() - Method in class forge.program.BinaryExpression

roots(Formula) - Static method in class forge.util.ExpressionUtil

Returns the non-trivial roots the formula.

run(ForgeBounds) - Method in class forge.solve.ForgeSolver

Finds a trace of the procedure within the given bounds.

run(ForgeCFG.Spec, ForgeBounds) - Method in class forge.solve.ForgeSolver

Finds a trace of the procedure within the given bounds that refines the given specification statement, determining coverage information in the case where no trace can be found if coverage flag is set to true.

runAll(ForgeCFG.Spec, ForgeBounds) - Method in class forge.solve.ForgeSolver

runAllTest() - Method in class forge.tests.ForgeTest

runSpec() - Method in class forge.tests.ForgeTest

runTest() - Method in class forge.tests.ForgeTest

S

satisfiable() - Method in class forge.solve.ForgeSolution

Returns true iff the solver found a satisfying trace.

satSolver(SolveOptions.SatSolver) - Method in class forge.solve.SolveOptions.Builder

Chooses the SAT solver.

satSolver() - Method in class forge.solve.SolveOptions

SEStrategy - Interface in forge.translate

The strategy for symbolic execution.

setBounds(int, Map<InstanceDomain, Integer>) - Method in class forge.tests.ForgeTest

setElse(CFGStmt) - Method in class forge.cfg.BranchStmt

setEntry(CFGStmt) - Method in class forge.cfg.ForgeCFG.Impl

Set the entry stmt of the implementation.

setNext(CFGStmt) - Method in class forge.cfg.UpdateStmt

setOfAtoms(TupleSet) - Method in class forge.util.RelationFactory

Wraps the given TupleSet of unary tuples as a set of atoms.

setOfTuples(TupleSet) - Method in class forge.util.RelationFactory

Wraps the given TupleSet as a set of tuples.

setThen(CFGStmt) - Method in class forge.cfg.BranchStmt

setUniverse(Set<O>) - Method in class forge.util.RelationFactory

shiftLeft(ForgeExpression) - Method in interface forge.program.ForgeExpression

shiftRight(ForgeExpression) - Method in interface forge.program.ForgeExpression

singleton(CFGStmt) - Static method in class forge.cfg.StmtSet

singletonTupleSet(O) - Method in class forge.util.RelationFactory

Returns a singleton TupleSet containing the given atom.

singletonTupleSet(Tuple) - Method in class forge.util.RelationFactory

Returns a singleton TupleSet containing the given tuple.

size() - Method in class forge.cfg.StmtSet

size() - Method in interface forge.program.ForgeExpression

skolemizing(Object, Object, List<?>) - Method in class forge.solve.ForgeReporter

Reports that Kodkod is skolemizing the declaration (kodkod.ast.Decl) using the given skolem relation (kodkod.ast.Relation).

skolemizing(Object, Object, List<?>) - Method in class forge.util.SystemOutReporter

slice(Formula) - Method in class forge.translate.ForgeTranslation

Returns the set of statements responsible for the given assume formula.

slice(ForgeExpression.Modifiable) - Method in class forge.translate.ForgeTranslation

Returns the set of statements that impact the given modifiable.

slices() - Method in class forge.translate.SymbolicExecutor

SolveOptions - Class in forge.solve

Forge solving options.

SolveOptions.Builder - Class in forge.solve

Builder for SolveOptions

SolveOptions.Builder(int) - Constructor for class forge.solve.SolveOptions.Builder

SolveOptions.Builder() - Constructor for class forge.solve.SolveOptions.Builder

SolveOptions.SatSolver - Enum in forge.solve

Enumeration of possible SAT Solvers.

solvingAnalysis() - Method in class forge.solve.ForgeReporter

Reports that Forge is about to invoke Kodkod to solve the analysis.

solvingAnalysis() - Method in class forge.util.SystemOutReporter

solvingCNF(int, int, int) - Method in class forge.solve.ForgeReporter

Reports that Kodkod generated a CNF consisting of the given number of variables and clauses, is being analyzed by a SAT solver.

solvingCNF(int, int, int) - Method in class forge.util.SystemOutReporter

some() - Method in interface forge.program.ForgeExpression

source() - Method in class forge.transform.AbstractTransformer.TransformVisitor

sourceStmt(CFGStmt) - Method in class forge.transform.AbstractTransformer

sourceStmt(CFGStmt) - Method in class forge.transform.BatchTransformer

sourceStmt(CFGStmt) - Method in interface forge.transform.Transformer

Returns the source update from which the given target was transformed.

sourceStmt(CFGStmt) - Method in class forge.transform.UnrollTransformer

spec() - Method in class forge.solve.Coverage

spec() - Method in class forge.solve.ForgeSolution

specification(ForgeProcedure, Set<GlobalVariable>, ForgeExpression) - Static method in class forge.cfg.ForgeCFG

Returns a new unmodifiable CFG that who entry is a specification stmt that modifies the union of the given globals and output parameters and with the given condition.

SpecStmt - Class in forge.cfg

A specification statement.

standardTest() - Method in class forge.tests.ForgeTest

Step - Class in forge.solve

A step in a trace.

Step.Branch - Class in forge.solve

A branch step: a BranchStmt and a truth value.

Step.Call - Class in forge.solve

A call step: an CallStmt with its own trace.

Step.Update - Class in forge.solve

An update step: an UpdateStmt and an effect.

steps() - Method in class forge.solve.Trace

stmt() - Method in class forge.solve.Step.Branch

stmt() - Method in class forge.solve.Step.Call

stmt() - Method in class forge.solve.Step

stmt() - Method in class forge.solve.Step.Update

stmtRelations() - Method in class forge.translate.RelationalModel

stmtScore(CFGStmt) - Method in class forge.solve.Coverage

StmtSet - Class in forge.cfg

A set of statements belonging to a single CFG.

StmtSet(ForgeCFG, Set<CFGStmt>) - Constructor for class forge.cfg.StmtSet

StoreException - Exception in forge.cfg

Checks if expression can be stored in an l-value.

strategy(SEStrategy) - Method in class forge.solve.SolveOptions.Builder

Choose the symbolic execution strategy.

strategy() - Method in class forge.solve.SolveOptions

STRATEGY - Static variable in class forge.translate.ConstrainStrategy

STRATEGY - Static variable in class forge.translate.HybridStrategy

STRATEGY - Static variable in class forge.translate.InlineStrategy

strategy() - Method in class forge.translate.SymbolicExecutor

StrategyComparison - Class in forge.tests

Compare the different translation strategies.

stringDomain() - Method in class forge.tests.RegisterTest

sub() - Method in class forge.program.ProjectionExpression

sub() - Method in class forge.program.QuantifyExpression

sub() - Method in class forge.program.UnaryExpression

subsetOf(ForgeConstant) - Method in interface forge.solve.ForgeConstant

Returns true if this is a subset of c

subtypeOf(ForgeType) - Method in interface forge.program.ForgeType

succs() - Method in class forge.cfg.BranchStmt

succs() - Method in class forge.cfg.CFGStmt

Returns an unmodifiable view of the successor stmts.

succs() - Method in class forge.cfg.ExitStmt

succs() - Method in class forge.cfg.ReferenceStmt

Returns an unmodifiable view of the successor stmts.

succs() - Method in class forge.cfg.UpdateStmt

sum() - Method in interface forge.program.ForgeExpression

sum() - Method in class forge.solve.BooleanAtom

sum() - Method in class forge.solve.InstanceAtom

sum() - Method in class forge.solve.IntegerAtom

summation(LocalDecls) - Method in interface forge.program.ForgeExpression

SymbolicExecutor - Class in forge.translate

Symbolically executes statements.

SymbolicExecutor(SEStrategy, Environment, SliceLog) - Constructor for class forge.translate.SymbolicExecutor

SymbolicExecutor.AssignHook - Class in forge.translate

Callback hook for execute(AssignStmt) method.

SymbolicExecutor.BranchHook - Class in forge.translate

Callback hook for the merge method.

SymbolicExecutor.CreateHook - Class in forge.translate

Callback hook for execute(CreateStmt) method.

SymbolicExecutor.SpecHook - Class in forge.translate

Callback hook for execute(AssignStmt) method.

SystemOutReporter - Class in forge.util

A reporter that prints out basic information to the standard out noting which phase of the translation it is in.

T

target() - Method in class forge.transform.AbstractTransformer.TransformVisitor

thenData() - Method in class forge.dataflow.BranchData

Returns the then data.

thenElse(ForgeExpression, ForgeExpression) - Method in interface forge.program.ForgeExpression

thenExpr() - Method in class forge.program.ConditionalExpression

ThesisStrategy - Class in forge.translate

ThesisStrategy(boolean, boolean, boolean) - Constructor for class forge.translate.ThesisStrategy

times(ForgeExpression) - Method in interface forge.program.ForgeExpression

timesCovered() - Method in class forge.solve.Coverage.Score

timesMissed() - Method in class forge.solve.Coverage.Score

timesTotal() - Method in class forge.solve.Coverage.Score

toArray() - Method in class forge.cfg.StmtSet

toArray(T[]) - Method in class forge.cfg.StmtSet

toAtom(O) - Method in class forge.util.RelationFactory

Converts an object stored in the universe to an atom.

toBooleanMatrix(TupleSet) - Method in class forge.util.RelationFactory

Converts a TupleSet to a BooleanMatrix.

toExpr(ForgeExpression) - Method in class forge.translate.ExprTranslator

Translates the given Forge expression to a Kodkod expression.

toExpr(ForgeExpression.Modifiable) - Method in class forge.translate.ExprTranslator

Faster translates for a modifiable.

toForm(ForgeExpression) - Method in class forge.translate.ExprTranslator

Translates the given Forge expression to a Kodkod formula.

toInt(ForgeExpression) - Method in class forge.translate.ExprTranslator

Translates the given Forge expression to a Kodkod integer expression.

TopologicalSortTest - Class in forge.tests

Analyzes TopologicalFIR

toString() - Method in class forge.cfg.CFGStmt

toString() - Method in class forge.cfg.ForgeCFG

toString() - Method in class forge.cfg.StmtSet

toString() - Method in class forge.dataflow.BranchData

toString() - Method in enum forge.program.BinaryExpression.Op

toString() - Method in class forge.program.BinaryExpression

toString() - Method in class forge.program.ConditionalExpression

toString() - Method in class forge.program.ForgeDomain

toString() - Method in class forge.program.ForgeLiteral

toString() - Method in class forge.program.ForgeProcedure

toString() - Method in class forge.program.ForgeVariable

toString() - Method in class forge.program.LocalDecls.EmptyDecls

toString() - Method in class forge.program.LocalDecls.MultiDecls

toString() - Method in class forge.program.OldExpression

toString() - Method in class forge.program.ProjectionExpression

toString() - Method in enum forge.program.QuantifyExpression.Op

toString() - Method in class forge.program.QuantifyExpression

toString() - Method in enum forge.program.UnaryExpression.Op

toString() - Method in class forge.program.UnaryExpression

toString() - Method in class forge.solve.Binding

toString() - Method in class forge.solve.Coverage.Score

toString() - Method in class forge.solve.Coverage

toString() - Method in class forge.solve.ForgeAtom

toString() - Method in class forge.solve.ForgeSolution

toString() - Method in class forge.solve.SolveOptions

toString() - Method in class forge.solve.Step.Branch

toString() - Method in class forge.solve.Step.Call

toString() - Method in class forge.solve.Step.Update

toString() - Method in class forge.solve.Trace

toString() - Method in class forge.tests.ForgeTest

toString() - Method in class forge.translate.ConstrainStrategy

toString() - Method in class forge.translate.Environment

toString() - Method in class forge.translate.HybridStrategy

toString() - Method in class forge.translate.InlineStrategy

toString() - Method in class forge.translate.ThesisStrategy

trace() - Method in class forge.solve.ForgeSolution

Returns the satisfying trace if unsatisfiable; otherwise null.

trace() - Method in class forge.solve.Step.Call

Trace - Class in forge.solve

A trace of a Forge procedure, a series of steps.

transfer(AssignStmt, D) - Method in class forge.dataflow.DataflowAnalysis

Transfer function at an assign stmt.

transfer(CallStmt, D) - Method in class forge.dataflow.DataflowAnalysis

Transfer function at a call stmt.

transfer(CreateStmt, D) - Method in class forge.dataflow.DataflowAnalysis

Transfer function at a create stmt.

transfer(SpecStmt, D) - Method in class forge.dataflow.DataflowAnalysis

Transfer function at an spec stmt.

transfer(BranchStmt, D) - Method in class forge.dataflow.DataflowAnalysis

Transfer function at a branch node.

transfer(ExitStmt, D) - Method in class forge.dataflow.DataflowAnalysis

Transfer function at a terminal node.

transfer(AssignStmt, Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

transfer(BranchStmt, Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

transfer(CallStmt, Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

transfer(CreateStmt, Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

transfer(SpecStmt, Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

transfer(ExitStmt, Set<CFGStmt>) - Method in class forge.dataflow.DominatorAnalysis

transfer(AssignStmt, Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

transfer(SpecStmt, Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

transfer(BranchStmt, Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

transfer(CallStmt, Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

transfer(CreateStmt, Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

transfer(ExitStmt, Set<CFGStmt>) - Method in class forge.dataflow.InverseDominatorAnalysis

transfer(AssignStmt, Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

transfer(BranchStmt, Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

transfer(CallStmt, Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

transfer(CreateStmt, Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

transfer(SpecStmt, Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

transfer(ExitStmt, Set<CFGStmt>) - Method in class forge.dataflow.ReachabilityAnalysis

transform(ForgeCFG) - Method in class forge.transform.AbstractTransformer

Checks in the cache whether or not the procedure has already been transformed.

transform(AssignStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Transforms the statement to a new statement or null, but must also call replace to set the result of an application to this statement.

transform(CreateStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Transforms the statement to a new statement or null, but must also call replace to set the result of an application to this statement.

transform(SpecStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Transforms the statement to a new statement or null, but must also call replace to set the result of an application to this statement.

transform(CallStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Transforms the statement to a new statement or null, but must also call replace to set the result of an application to this statement.

transform(BranchStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Transforms the statement to a new statement or null, but must also call replace to set the result of an application to this statement.

transform(ExitStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

Transforms the statement to a new statement or null, but must also call replace to set the result of an application to this statement.

transform(ForgeCFG) - Method in class forge.transform.BatchTransformer

transform(ForgeCFG) - Method in interface forge.transform.Transformer

Performs the transformation and returns the transformed procedure.

transform(ForgeCFG) - Method in class forge.transform.UnrollTransformer

transformer(Transformer) - Method in class forge.solve.SolveOptions.Builder

Choose the transformer.

transformer() - Method in class forge.solve.SolveOptions

Transformer - Interface in forge.transform

Transforms a cfg, either in place, or by creating a new cfg.

transformingProcedure() - Method in class forge.solve.ForgeReporter

Reports that Forge is transforming the procedure.

transformingProcedure() - Method in class forge.util.SystemOutReporter

translate(SEStrategy, ForgeCFG, boolean) - Static method in class forge.translate.ForgeTranslation

Translates the given cfg to Kodkod, logging the slice information iff the logSlices flag is true.

translatingToBoolean(Object, Object) - Method in class forge.solve.ForgeReporter

Reports that Kodkod is translating the given formula (kodkod.ast.Formula) and bounds (kodkod.instance.Bounds) to a boolean circuit.

translatingToBoolean(Object, Object) - Method in class forge.util.SystemOutReporter

translatingToCNF(Object) - Method in class forge.solve.ForgeReporter

Reports that Kodkod is translating the given boolean circuit (kodkod.engine.bool.BooleanFormula) to CNF.

translatingToCNF(Object) - Method in class forge.util.CircuitReporter

Dumps the given circuit to this.file, in eDIMACS format, if the circuit is not just a variable.

translatingToCNF(Object) - Method in class forge.util.SystemOutReporter

translatingToKodkod() - Method in class forge.solve.ForgeReporter

Reports that Forge is translating the procedure to Kodkod.

translatingToKodkod() - Method in class forge.util.SystemOutReporter

traverse(ForgeCFG) - Method in class forge.util.BreadthFirstVisitor

Performs a breadth-first traversal of the cfgs in the call graph, and then of the statements within each cfg.

treeDomain() - Method in class forge.tests.TreeIntSetTest

TreeIntSetTest - Class in forge.tests

Insertion into a binary tree integer set.

TreeIntSetTest() - Constructor for class forge.tests.TreeIntSetTest

TreeIntSetTest2 - Class in forge.tests

Insertion into a binary tree integer set.

TreeIntSetTest2() - Constructor for class forge.tests.TreeIntSetTest2

trueLiteral() - Method in class forge.program.ForgeProgram

Returns the true literal.

trueRelation() - Method in class forge.translate.RelationalModel

truth() - Method in class forge.solve.Step.Branch

tuple(A...) - Method in class forge.util.RelationFactory

Constructs a Tuple with the given atoms.

tuples() - Method in interface forge.solve.ForgeConstant

Returns the set of tuples in this constant

tuples() - Method in interface forge.solve.ForgeConstant.Unary

tupleSet() - Method in interface forge.solve.ForgeConstant

tupleTypes() - Method in interface forge.program.ForgeType

tupleTypes() - Method in interface forge.program.ForgeType.Unary

type() - Method in class forge.cfg.CreateStmt

type() - Method in class forge.program.BinaryExpression

type() - Method in class forge.program.BooleanLiteral

type() - Method in class forge.program.ConditionalExpression

type() - Method in interface forge.program.ForgeExpression

Returns the type of this expression.

type() - Method in class forge.program.ForgeLiteral

type() - Method in class forge.program.ForgeVariable

type() - Method in class forge.program.InstanceLiteral

type() - Method in class forge.program.IntegerLiteral

type() - Method in class forge.program.OldExpression

type() - Method in class forge.program.ProjectionExpression

type() - Method in class forge.program.QuantifyExpression

type() - Method in class forge.program.UnaryExpression

type() - Method in class forge.solve.BooleanAtom

type() - Method in class forge.solve.ForgeAtom

type() - Method in interface forge.solve.ForgeConstant.Tuple

type() - Method in interface forge.solve.ForgeConstant

Returns the type of this constant.

type() - Method in interface forge.solve.ForgeConstant.Unary

type() - Method in class forge.solve.InstanceAtom

type() - Method in class forge.solve.IntegerAtom

U

UnaryExpression - Class in forge.program

An expression composed of a unary operator and a subexpression.

UnaryExpression.Op - Enum in forge.program

union(ForgeExpression) - Method in interface forge.program.ForgeExpression

union(ForgeType) - Method in interface forge.program.ForgeType.Unary

union(ForgeType) - Method in interface forge.program.ForgeType

union(ForgeConstant) - Method in interface forge.solve.ForgeConstant.Unary

union(ForgeConstant) - Method in interface forge.solve.ForgeConstant

unionTupleSet(BooleanMatrix, BooleanMatrix) - Method in class forge.util.RelationFactory

Returns TupleSet that is the union of two matrices.

universe() - Method in class forge.util.RelationFactory

Return the kodkod universe used by this factory.

unmodifiable() - Method in class forge.cfg.StmtSet

unmodifiable() - Method in class forge.translate.Environment

unmodifiable() - Method in class forge.util.ModifiableMap

unmodifiableView() - Method in class forge.solve.Binding

Returns an unmodifiable view of this binding.

unpinOldExprs() - Method in class forge.translate.ExprTranslator

Unpins all the old expressions.

UnrollTransformer - Class in forge.transform

Transformer that unrolls loops of the procedure and all called procedures.

UnrollTransformer(int) - Constructor for class forge.transform.UnrollTransformer

Constructs a loop unroller that unrolls for the given number of times.

unsignedShiftRight(ForgeExpression) - Method in interface forge.program.ForgeExpression

UpdateStmt - Class in forge.cfg

A stmt in the control flow graph that may change the state of the execution and which has exactly one successor.

userDomain() - Method in class forge.tests.RegisterTest

V

value() - Method in class forge.program.BooleanLiteral

value() - Method in class forge.program.IntegerLiteral

value() - Method in class forge.solve.BooleanAtom

value() - Method in class forge.solve.IntegerAtom

valueOf(String) - Static method in enum forge.program.BinaryExpression.Op

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum forge.program.ForgeDomain.Kind

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum forge.program.QuantifyExpression.Op

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum forge.program.UnaryExpression.Op

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum forge.solve.SolveOptions.SatSolver

Returns the enum constant of this type with the specified name.

values() - Static method in enum forge.program.BinaryExpression.Op

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum forge.program.ForgeDomain.Kind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum forge.program.QuantifyExpression.Op

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum forge.program.UnaryExpression.Op

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum forge.solve.SolveOptions.SatSolver

Returns an array containing the constants of this enum type, in the order they are declared.

var() - Method in class forge.cfg.AssignStmt

var() - Method in class forge.cfg.CreateStmt

variable() - Method in class forge.program.OldExpression

visit(AssignStmt) - Method in interface forge.cfg.CFGVisitor

Visits an AssignStmt in the CFG.

visit(CallStmt) - Method in interface forge.cfg.CFGVisitor

Visits a CallStmt in the CFG.

visit(CreateStmt) - Method in interface forge.cfg.CFGVisitor

Visits a CreateStmt in the CFG.

visit(BranchStmt) - Method in interface forge.cfg.CFGVisitor

Visits a BranchStmt in the CFG.

visit(SpecStmt) - Method in interface forge.cfg.CFGVisitor

Visits a SpecStmt in the CFG.

visit(ExitStmt) - Method in interface forge.cfg.CFGVisitor

Visits a ExitStmt in the CFG.

visit(ForgeType) - Method in class forge.program.ExpressionVisitor

Visits a ForgeType.

visit(ForgeLiteral) - Method in class forge.program.ExpressionVisitor

Visits a ForgeConstant.

visit(ForgeVariable) - Method in class forge.program.ExpressionVisitor

Visits a ForgeVariable.

visit(UnaryExpression) - Method in class forge.program.ExpressionVisitor

Visits a UnaryExpression.

visit(BinaryExpression) - Method in class forge.program.ExpressionVisitor

Visits a BinaryExpression.

visit(ConditionalExpression) - Method in class forge.program.ExpressionVisitor

Visits a ConditionalExpression.

visit(ProjectionExpression) - Method in class forge.program.ExpressionVisitor

Visits a ProjectionExpression.

visit(QuantifyExpression) - Method in class forge.program.ExpressionVisitor

Visits a QuantifyExpression.

visit(OldExpression) - Method in class forge.program.ExpressionVisitor

Visits an OldExpression.

visit(AssignStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

visit(BranchStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

visit(CallStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

visit(CreateStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

visit(ExitStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

visit(SpecStmt) - Method in class forge.transform.AbstractTransformer.TransformVisitor

visit(ForgeType) - Method in class forge.transform.ExpressionDefaulter

visit(ForgeLiteral) - Method in class forge.transform.ExpressionDefaulter

visit(ForgeVariable) - Method in class forge.transform.ExpressionDefaulter

visit(UnaryExpression) - Method in class forge.transform.ExpressionDefaulter

visit(BinaryExpression) - Method in class forge.transform.ExpressionDefaulter

visit(ConditionalExpression) - Method in class forge.transform.ExpressionDefaulter

visit(ProjectionExpression) - Method in class forge.transform.ExpressionDefaulter

visit(QuantifyExpression) - Method in class forge.transform.ExpressionDefaulter

visit(OldExpression) - Method in class forge.transform.ExpressionDefaulter

visit(BinaryExpression) - Method in class forge.transform.ExpressionDescender

visit(UnaryExpression) - Method in class forge.transform.ExpressionDescender

visit(ConditionalExpression) - Method in class forge.transform.ExpressionDescender

visit(QuantifyExpression) - Method in class forge.transform.ExpressionDescender

visit(ProjectionExpression) - Method in class forge.transform.ExpressionDescender

visit(OldExpression) - Method in class forge.transform.ExpressionDescender

visit(ForgeLiteral) - Method in class forge.transform.ExpressionDescender

visit(ForgeType) - Method in class forge.transform.ExpressionDescender

visit(ForgeVariable) - Method in class forge.transform.ExpressionDescender

visit(UnaryExpression) - Method in class forge.transform.ExpressionReplacer

visit(BinaryExpression) - Method in class forge.transform.ExpressionReplacer

visit(ConditionalExpression) - Method in class forge.transform.ExpressionReplacer

visit(ProjectionExpression) - Method in class forge.transform.ExpressionReplacer

visit(QuantifyExpression) - Method in class forge.transform.ExpressionReplacer

visit(OldExpression) - Method in class forge.transform.ExpressionReplacer

visit(ForgeLiteral) - Method in class forge.transform.ExpressionReplacer

visit(ForgeType) - Method in class forge.transform.ExpressionReplacer

visit(ForgeVariable) - Method in class forge.transform.ExpressionReplacer

visit(ForgeCFG) - Method in class forge.util.BreadthFirstVisitor

visit(AssignStmt) - Method in class forge.util.BreadthFirstVisitor

visit(BranchStmt) - Method in class forge.util.BreadthFirstVisitor

visit(CallStmt) - Method in class forge.util.BreadthFirstVisitor

visit(CreateStmt) - Method in class forge.util.BreadthFirstVisitor

visit(ExitStmt) - Method in class forge.util.BreadthFirstVisitor

visit(SpecStmt) - Method in class forge.util.BreadthFirstVisitor

visitor(ForgeCFG) - Method in class forge.transform.AbstractTransformer

Returns a TransformVisitor that converts source.

visitor(ForgeCFG) - Method in class forge.transform.InlineTransformer

W

weak(ForgeCFG) - Static method in class forge.cfg.StmtSet

X

xor(ForgeExpression) - Method in interface forge.program.ForgeExpression

Z

ZuneTest - Class in forge.tests

ZuneTest() - Constructor for class forge.tests.ZuneTest

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