de.uka.ilkd.key.rule.conditions

Class StaticMethodCondition

java.lang.Object

de.uka.ilkd.key.rule.VariableConditionAdapter

de.uka.ilkd.key.rule.conditions.StaticMethodCondition

All Implemented Interfaces:

VariableCondition

public final class StaticMethodCondition
extends VariableConditionAdapter

ensures that the given instantiation for the schemavariable denotes a static method. For determining the method the callee and the arguments of the method are needed as arguments.

Field Summary

Fields

Modifier and Type	Field and Description
private SchemaVariable	args
private SchemaVariable	caller
private SchemaVariable	methname
private boolean	negation

Constructor Summary

Constructors

Constructor and Description
StaticMethodCondition(boolean negation, SchemaVariable caller, SchemaVariable methname, SchemaVariable args) the static reference condition checks if a suggested instantiation for a schema variable denotes a static method call.

Method Summary

Modifier and Type	Method and Description
boolean	check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, Services services) checks if the condition for a correct instantiation is fulfilled
private static ImmutableArray<Expression>	toExpArray(ImmutableArray<? extends ProgramElement> a)
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.rule.VariableConditionAdapter

check

Methods inherited from class java.lang.Object

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

Field Detail

negation

private final boolean negation

caller

private final SchemaVariable caller

methname

private final SchemaVariable methname

args

private final SchemaVariable args

Constructor Detail

StaticMethodCondition

public StaticMethodCondition(boolean negation,
                             SchemaVariable caller,
                             SchemaVariable methname,
                             SchemaVariable args)

the static reference condition checks if a suggested instantiation for a schema variable denotes a static method call. The flag negation allows to reuse this condition for ensuring non static references.

Method Detail

toExpArray

private static ImmutableArray<Expression> toExpArray(ImmutableArray<? extends ProgramElement> a)

check

public boolean check(SchemaVariable var,
                     SVSubstitute subst,
                     SVInstantiations svInst,
                     Services services)

Description copied from class: VariableConditionAdapter

checks if the condition for a correct instantiation is fulfilled

Specified by:

check in class VariableConditionAdapter

Parameters:

var - the template Variable to be instantiated

svInst - the MatchCondition with the current matching state and in particular the SVInstantiations that are already known to be needed

services - the program information object

Returns:

true iff condition is fulfilled

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object