de.uka.ilkd.key.symbolic_execution.util

Class SymbolicExecutionUtil.SiteProofVariableValueInput

java.lang.Object

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

Enclosing class:

SymbolicExecutionUtil

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

Helper class which represents the return value of ExecutionMethodReturn#createExtractReturnVariableValueSequent(TypeReference, ReferencePrefix, Node, IProgramVariable) and ExecutionMethodReturn#createExtractVariableValueSequent(IExecutionContext, Node, IProgramVariable).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Operator	operator The Operator which is the predicate that contains the value interested in.
private Sequent	sequentToProve The sequent to prove.

Constructor Summary

Constructors

Constructor and Description
SiteProofVariableValueInput(Sequent sequentToProve, Operator operator) Constructor.

Method Summary

Modifier and Type	Method and Description
Operator	getOperator() Returns the Operator which is the predicate that contains the value interested in.
Sequent	getSequentToProve() Returns the sequent to prove.

Methods inherited from class java.lang.Object

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

Field Detail

sequentToProve

private Sequent sequentToProve

The sequent to prove.

operator

private Operator operator

The Operator which is the predicate that contains the value interested in.

Constructor Detail

SiteProofVariableValueInput

public SiteProofVariableValueInput(Sequent sequentToProve,
                                   Operator operator)

Constructor.

Parameters:

sequentToProve - he sequent to prove.

operator - The Operator which is the predicate that contains the value interested in.

Method Detail

getSequentToProve

public Sequent getSequentToProve()

Returns the sequent to prove.

Returns:

The sequent to prove.

getOperator

public Operator getOperator()

Returns the Operator which is the predicate that contains the value interested in.

Returns:

The Operator which is the predicate that contains the value interested in.