de.uka.ilkd.key.symbolic_execution.slicing

Class AbstractSlicer.SequentInfo

java.lang.Object

de.uka.ilkd.key.symbolic_execution.slicing.AbstractSlicer.SequentInfo

Enclosing class:

AbstractSlicer

protected static class AbstractSlicer.SequentInfo
extends java.lang.Object

The result returned by AbstractSlicer#analyzeSequent(Node).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<Location,java.util.SortedSet<Location>>	aliases The found aliases.
private ExecutionContext	executionContext The current ExecutionContext.
private java.util.Map<ProgramVariable,Term>	localValues The local values.
private ReferencePrefix	thisReference The this reference if available.

Constructor Summary

Constructors

Constructor and Description
SequentInfo(java.util.Map<Location,java.util.SortedSet<Location>> aliases, java.util.Map<ProgramVariable,Term> localValues, ExecutionContext executionContext, ReferencePrefix thisReference) Constructor.

Method Summary

Modifier and Type	Method and Description
java.util.Map<Location,java.util.SortedSet<Location>>	getAliases() Returns the found aliases.
ExecutionContext	getExecutionContext() Returns the current ExecutionContext.
java.util.Map<ProgramVariable,Term>	getLocalValues() Returns the local values.
ReferencePrefix	getThisReference() Returns the this reference if available.

Methods inherited from class java.lang.Object

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

Field Detail

aliases

private final java.util.Map<Location,java.util.SortedSet<Location>> aliases

The found aliases.

localValues

private final java.util.Map<ProgramVariable,Term> localValues

The local values.

executionContext

private final ExecutionContext executionContext

The current ExecutionContext.

thisReference

private final ReferencePrefix thisReference

The this reference if available.

Constructor Detail

SequentInfo

public SequentInfo(java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                   java.util.Map<ProgramVariable,Term> localValues,
                   ExecutionContext executionContext,
                   ReferencePrefix thisReference)

Constructor.

Parameters:

aliases - The found aliases.

thisReference - The this reference if available.

Method Detail

getAliases

public java.util.Map<Location,java.util.SortedSet<Location>> getAliases()

Returns the found aliases.

Returns:

The found aliases.

getLocalValues

public java.util.Map<ProgramVariable,Term> getLocalValues()

Returns the local values.

Returns:

The local values.

getExecutionContext

public ExecutionContext getExecutionContext()

Returns the current ExecutionContext.

Returns:

The current ExecutionContext.

getThisReference

public ReferencePrefix getThisReference()

Returns the this reference if available.

Returns:

The this reference if available.