public class ProofObligationVars
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
Term |
exceptionParameter
Exception Variable for the try-catch statement.
|
ImmutableList<Term> |
formalParams
The formal parameters of a method.
|
StateVars |
post
Variables for the pre and post condition.
|
java.lang.String |
postfix
If this object was created form another ProofObligationVars
object by adding a postfix to the variable names, then this
variable contains the used postfix.
|
StateVars |
pre
Variables for the pre and post condition.
|
private TermBuilder |
tb |
Constructor and Description |
---|
ProofObligationVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
ProofObligationVars(ProofObligationVars orig,
java.lang.String postfix,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
Services services) |
ProofObligationVars(StateVars pre,
StateVars post,
Term exceptionParameter,
ImmutableList<Term> formalParams,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
private Term |
buildExceptionParameter(Services services)
Build variable for try statement.
|
private ImmutableList<Term> |
buildFormalParamVars(Services services)
Create formal parameters.
|
ProofObligationVars |
labelHeapAtPreAsAnonHeapFunc() |
(package private) static void |
register(ProgramVariable pv,
Services services) |
public final StateVars pre
public final StateVars post
public final Term exceptionParameter
public final ImmutableList<Term> formalParams
public final java.lang.String postfix
private final TermBuilder tb
public ProofObligationVars(IProgramMethod pm, KeYJavaType kjt, Services services)
public ProofObligationVars(ProofObligationVars orig, java.lang.String postfix, Services services)
public ProofObligationVars(StateVars pre, StateVars post, Term exceptionParameter, ImmutableList<Term> formalParams, Services services)
public ProofObligationVars(StateVars pre, StateVars post, Term exceptionParameter, ImmutableList<Term> formalParams, TermBuilder tb)
public ProofObligationVars labelHeapAtPreAsAnonHeapFunc()
private Term buildExceptionParameter(Services services)
services
- the services object.private ImmutableList<Term> buildFormalParamVars(Services services) throws java.lang.IllegalArgumentException
java.lang.IllegalArgumentException
static void register(ProgramVariable pv, Services services)