de.uka.ilkd.key.symbolic_execution.util

Class SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult

java.lang.Object

de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult

Enclosing class:

SymbolicExecutionUtil

public static class SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult
extends java.lang.Object

The result of SymbolicExecutionUtil.searchContractPostOrExcPostExceptionVariable(Node, Services).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	exceptionDefinition The exception definition.
private Term	exceptionEquality The equality which contains the equality.
private Pair<ImmutableList<Term>,Term>	updatesAndTerm The updates.
private Term	workingTerm The working Term.

Constructor Summary

Constructors

Constructor and Description
ContractPostOrExcPostExceptionVariableResult(Term workingTerm, Pair<ImmutableList<Term>,Term> updatesAndTerm, Term exceptionDefinition, Term exceptionEquality) Constructor.

Method Summary

Modifier and Type	Method and Description
Term	getExceptionDefinition() Returns the exception definition.
Term	getExceptionEquality() Returns the equality which contains the equality.
Pair<ImmutableList<Term>,Term>	getUpdatesAndTerm() Returns the updates.
Term	getWorkingTerm() Returns the working Term.

Methods inherited from class java.lang.Object

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

Field Detail

workingTerm

private Term workingTerm

The working Term.

updatesAndTerm

private Pair<ImmutableList<Term>,Term> updatesAndTerm

The updates.

exceptionDefinition

private Term exceptionDefinition

The exception definition.

exceptionEquality

private Term exceptionEquality

The equality which contains the equality.

Constructor Detail

ContractPostOrExcPostExceptionVariableResult

public ContractPostOrExcPostExceptionVariableResult(Term workingTerm,
                                                    Pair<ImmutableList<Term>,Term> updatesAndTerm,
                                                    Term exceptionDefinition,
                                                    Term exceptionEquality)

Constructor.

Parameters:

workingTerm - The working Term.

updatesAndTerm - The updates.

exceptionDefinition - The exception definition.

exceptionEquality - The equality which contains the equality.

Method Detail

getWorkingTerm

public Term getWorkingTerm()

Returns the working Term.

Returns:

The working Term.

getUpdatesAndTerm

public Pair<ImmutableList<Term>,Term> getUpdatesAndTerm()

Returns the updates.

Returns:

The updates.

getExceptionDefinition

public Term getExceptionDefinition()

Returns the exception definition.

Returns:

The exception definition.

getExceptionEquality

public Term getExceptionEquality()

Returns the equality which contains the equality.

Returns:

The equality which contains the equality.