public class StateVars
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
Term |
exception |
Term |
guard |
Term |
heap |
ImmutableList<Term> |
localVars |
Term |
mbyAtPre |
ImmutableList<Term> |
paddedTermList |
Term |
result |
Term |
self |
ImmutableList<Term> |
termList |
Constructor and Description |
---|
StateVars(StateVars orig,
java.lang.String postfix,
Services services) |
StateVars(Term self,
ImmutableList<Term> localVars,
Term heap) |
StateVars(Term self,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap) |
StateVars(Term self,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap,
Term mbyAtPre) |
StateVars(Term self,
Term guard,
ImmutableList<Term> localVars,
Term heap) |
StateVars(Term self,
Term guard,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap) |
StateVars(Term self,
Term guard,
ImmutableList<Term> localVars,
Term result,
Term exception,
Term heap,
Term mbyAtPre) |
Modifier and Type | Method and Description |
---|---|
private ImmutableList<Term> |
appendIfNotNull(ImmutableList<Term> list,
ImmutableList<Term> list2) |
private ImmutableList<Term> |
appendIfNotNull(ImmutableList<Term> list,
Term t) |
private static Term |
buildExceptionVar(Services services,
java.lang.String postfix,
IProgramMethod pm) |
private static Term |
buildHeapFunc(java.lang.String postfix,
ImmutableArray<TermLabel> labels,
Services services) |
static StateVars |
buildInfFlowPostVars(StateVars origPreVars,
StateVars origPostVars,
StateVars preVars,
java.lang.String postfix,
Services services) |
static StateVars |
buildInfFlowPreVars(StateVars origPreVars,
java.lang.String postfix,
Services services) |
private static Term |
buildMbyVar(java.lang.String postfix,
Services services) |
static StateVars |
buildMethodContractPostVars(StateVars preVars,
IProgramMethod pm,
KeYJavaType kjt,
Services services) |
static StateVars |
buildMethodContractPreVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
private static ImmutableList<Term> |
buildParamVars(Services services,
java.lang.String postfix,
IProgramMethod pm) |
private static Term |
buildResultVar(IProgramMethod pm,
Services services,
java.lang.String postfix) |
private static Term |
buildSelfVar(Services services,
IProgramMethod pm,
KeYJavaType kjt,
java.lang.String postfix) |
private static Term |
copyFunction(Term t,
java.lang.String postfix,
Services services) |
private static Term |
copyHeapSymbol(Term t,
java.lang.String postfix,
Services services) |
private static Term |
copyVariable(Term t,
java.lang.String postfix,
Services services) |
private static ImmutableList<Term> |
copyVariables(ImmutableList<Term> ts,
java.lang.String postfix,
Services services) |
private static Term |
newFunction(Term t,
java.lang.String name,
Services services) |
private static Term |
newHeapSymbol(Term t,
java.lang.String name,
Services services) |
private static Term |
newVariable(Term t,
java.lang.String name,
Services services) |
(package private) static <T> ImmutableList<T> |
ops(ImmutableList<Term> terms,
java.lang.Class<T> opClass) |
(package private) static void |
register(Function f,
Services services) |
(package private) static void |
register(ImmutableList<ProgramVariable> pvs,
Services services) |
(package private) static void |
register(ProgramVariable pv,
Services services) |
java.lang.String |
toString() |
public final ImmutableList<Term> termList
public final ImmutableList<Term> paddedTermList
public final Term self
public final Term guard
public final ImmutableList<Term> localVars
public final Term result
public final Term exception
public final Term heap
public final Term mbyAtPre
public StateVars(Term self, Term guard, ImmutableList<Term> localVars, Term result, Term exception, Term heap, Term mbyAtPre)
public StateVars(Term self, ImmutableList<Term> localVars, Term result, Term exception, Term heap, Term mbyAtPre)
public StateVars(Term self, Term guard, ImmutableList<Term> localVars, Term heap)
public StateVars(Term self, Term guard, ImmutableList<Term> localVars, Term result, Term exception, Term heap)
public StateVars(Term self, ImmutableList<Term> localVars, Term result, Term exception, Term heap)
public StateVars(Term self, ImmutableList<Term> localVars, Term heap)
private ImmutableList<Term> appendIfNotNull(ImmutableList<Term> list, Term t)
private ImmutableList<Term> appendIfNotNull(ImmutableList<Term> list, ImmutableList<Term> list2)
private static ImmutableList<Term> copyVariables(ImmutableList<Term> ts, java.lang.String postfix, Services services)
private static Term copyHeapSymbol(Term t, java.lang.String postfix, Services services)
public static StateVars buildMethodContractPreVars(IProgramMethod pm, KeYJavaType kjt, Services services)
public static StateVars buildMethodContractPostVars(StateVars preVars, IProgramMethod pm, KeYJavaType kjt, Services services)
public static StateVars buildInfFlowPreVars(StateVars origPreVars, java.lang.String postfix, Services services)
public static StateVars buildInfFlowPostVars(StateVars origPreVars, StateVars origPostVars, StateVars preVars, java.lang.String postfix, Services services)
private static Term buildSelfVar(Services services, IProgramMethod pm, KeYJavaType kjt, java.lang.String postfix)
private static ImmutableList<Term> buildParamVars(Services services, java.lang.String postfix, IProgramMethod pm)
private static Term buildResultVar(IProgramMethod pm, Services services, java.lang.String postfix)
private static Term buildHeapFunc(java.lang.String postfix, ImmutableArray<TermLabel> labels, Services services)
private static Term buildExceptionVar(Services services, java.lang.String postfix, IProgramMethod pm)
static void register(ProgramVariable pv, Services services)
static void register(ImmutableList<ProgramVariable> pvs, Services services)
static <T> ImmutableList<T> ops(ImmutableList<Term> terms, java.lang.Class<T> opClass) throws java.lang.IllegalArgumentException
java.lang.IllegalArgumentException
public java.lang.String toString()
toString
in class java.lang.Object