de.uka.ilkd.key.java.visitor

Class ProgramSVCollector

java.lang.Object

de.uka.ilkd.key.java.visitor.JavaASTWalker

de.uka.ilkd.key.java.visitor.ProgramSVCollector

public class ProgramSVCollector
extends JavaASTWalker

This visitor is used to collect all appearing SchemaVariables in a java program

Field Summary

Fields

Modifier and Type	Field and Description
private SVInstantiations	instantiations the instantiations needed for unwind loop constructs
private ImmutableList<SchemaVariable>	result

Constructor Summary

Constructors

Constructor and Description
ProgramSVCollector(ProgramElement root, ImmutableList<SchemaVariable> vars) create the ProgramSVCollector
ProgramSVCollector(ProgramElement root, ImmutableList<SchemaVariable> vars, SVInstantiations svInst) create the ProgramSVCollector

Method Summary

Modifier and Type	Method and Description
protected void	doAction(ProgramElement node) the action that is performed just before leaving the node the last time.
ImmutableList<SchemaVariable>	getSchemaVariables()
void	start() starts the walker

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTWalker

depth, root, walk

Methods inherited from class java.lang.Object

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

Field Detail

result

private ImmutableList<SchemaVariable> result

instantiations

private SVInstantiations instantiations

the instantiations needed for unwind loop constructs

Constructor Detail

ProgramSVCollector

public ProgramSVCollector(ProgramElement root,
                          ImmutableList<SchemaVariable> vars)

create the ProgramSVCollector

Parameters:

root - the ProgramElement where to begin

vars - the IList where to add the new found ones

ProgramSVCollector

public ProgramSVCollector(ProgramElement root,
                          ImmutableList<SchemaVariable> vars,
                          SVInstantiations svInst)

create the ProgramSVCollector

Parameters:

root - the ProgramElement where to begin

vars - the IList where to add the new found ones

svInst - the SVInstantiations previously found in order to determine the needed labels for the UnwindLoop construct.

Method Detail

start

public void start()

starts the walker

Overrides:

start in class JavaASTWalker

getSchemaVariables

public ImmutableList<SchemaVariable> getSchemaVariables()

doAction

protected void doAction(ProgramElement node)

the action that is performed just before leaving the node the last time. Not only schema variables must be taken into consideration, but also program meta constructs with implicit schema variables containment

Specified by:

doAction in class JavaASTWalker

See Also:

ProgramTransformerWithSV