Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
IExecutionContext context,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
TypeReference contextObjectType,
IProgramMethod contextMethod,
ReferencePrefix contextObject,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractTermSequent(Services sideProofServices,
Node node,
PosInOccurrence pio,
Term additionalConditions,
Term term,
boolean keepUpdates)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractVariableValueSequent(Services services,
Node node,
PosInOccurrence pio,
Term additionalConditions,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
Copyright © 2003-2019 The KeY-Project.