de.uka.ilkd.key.strategy.feature

Class ThrownExceptionFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.ThrownExceptionFeature

All Implemented Interfaces:

Feature

public class ThrownExceptionFeature
extends BinaryFeature

Field Summary

Fields

Modifier and Type	Field and Description
private Sort[]	filteredExceptions

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ThrownExceptionFeature(java.lang.String[] p_filteredExceptions, Services services) creates a feature filtering first active throw statements where the thrown exception is of one of the given types (or their subtypes)

Method Summary

Modifier and Type	Method and Description
private boolean	blockedExceptions(Sort excType)
static Feature	create(java.lang.String[] blockedExceptions, Services services)
protected boolean	filter(RuleApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
protected boolean	filter(Term term, Services services, ExecutionContext ec)
private ProgramElement	getFirstExecutableStatement(Term term) returns the first executable statement (often identical with the first active statement)

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

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

Field Detail

filteredExceptions

private final Sort[] filteredExceptions

Constructor Detail

ThrownExceptionFeature

private ThrownExceptionFeature(java.lang.String[] p_filteredExceptions,
                               Services services)

creates a feature filtering first active throw statements where the thrown exception is of one of the given types (or their subtypes)

Parameters:

p_filteredExceptions - the String array with the types of the thrown exceptions

services - the Services

Method Detail

create

public static Feature create(java.lang.String[] blockedExceptions,
                             Services services)

blockedExceptions

private boolean blockedExceptions(Sort excType)

filter

protected boolean filter(RuleApp app,
                         PosInOccurrence pos,
                         Goal goal)

Description copied from class: BinaryFeature

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryFeature

Parameters:

app - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.

filter

protected boolean filter(Term term,
                         Services services,
                         ExecutionContext ec)

getFirstExecutableStatement

private ProgramElement getFirstExecutableStatement(Term term)

returns the first executable statement (often identical with the first active statement)

Parameters:

term - the Term with the program at top level

Returns:

the first executable statement