public final class SymbolicExecutionUtil
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult
The result of
searchContractPostOrExcPostExceptionVariable(Node, Services) . |
static class |
SymbolicExecutionUtil.SiteProofVariableValueInput
Helper class which represents the return value of
ExecutionMethodReturn#createExtractReturnVariableValueSequent(TypeReference, ReferencePrefix, Node, IProgramVariable) and
ExecutionMethodReturn#createExtractVariableValueSequent(IExecutionContext, Node, IProgramVariable) . |
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
CHOICE_SETTING_RUNTIME_EXCEPTIONS
Key for the choice option "runtimeExceptions".
|
static java.lang.String |
CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW
Value in choice option "runtimeExceptions" to allow exceptions.
|
static java.lang.String |
CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN
Value in choice option "runtimeExceptions" to ban exceptions.
|
static TermLabel |
LOOP_BODY_LABEL
Label attached to the modality which executes a loop body in branch
"Body Preserves Invariant" of applied "Loop Invariant" rules.
|
static Name |
LOOP_BODY_LABEL_NAME
Name of
LOOP_BODY_LABEL . |
static TermLabel |
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
Label attached to the implication when a loop body execution terminated
normally without any exceptions, returns or breaks in branch
"Body Preserves Invariant" of applied "Loop Invariant" rules to show the
loop invariant.
|
static Name |
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME
Name of
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL . |
static TermLabel |
RESULT_LABEL
Label attached to a
Term to evaluate in a side proof. |
static Name |
RESULT_LABEL_NAME
Name of
RESULT_LABEL . |
Modifier and Type | Method and Description |
---|---|
static boolean |
canComputeVariables(IExecutionNode<?> node,
Services services)
Checks if it is right now possible to compute the variables of the given
IExecutionNode
via IExecutionNode.getVariables() . |
static int |
checkSkolemEquality(SequentFormula sf)
Checks if the given
SequentFormula is a skolem equality. |
static int |
checkSkolemEquality(Term term)
Checks if the given
Term is a skolem equality. |
static java.util.List<IProgramVariable> |
collectAllElementaryUpdateTerms(Node node)
Collects all
IProgramVariable used in ElementaryUpdate s. |
static ImmutableList<Term> |
collectElementaryUpdates(Term term)
Collects the
ElementaryUpdate s in the given Term . |
static ImmutableList<Goal> |
collectGoalsInSubtree(IExecutionElement executionElement)
Collects all
Goal s in the subtree of the given IExecutionElement . |
static ImmutableList<Goal> |
collectGoalsInSubtree(Node node)
|
static Term |
computeBranchCondition(Node node,
boolean simplify,
boolean improveReadability)
Computes the branch condition of the given
Node . |
static Term |
computePathCondition(Node node,
boolean simplify,
boolean improveReadability)
Computes the path condition of the given
Node . |
static Term |
computePathCondition(Node parentNode,
Node childNode,
boolean simplify,
boolean improveReadability)
Computes the path condition between the given
Node s. |
static ImmutableList<Term> |
computeRootElementaryUpdates(Node root)
Computes the initial
ElementaryUpdate s on the given root Node . |
static Pair<java.lang.Integer,SourceElement> |
computeSecondStatement(RuleApp ruleApp)
Computes the call stack size and the second statement
similar to
NodeInfo.computeActiveStatement(SourceElement) . |
static int |
computeStackSize(RuleApp ruleApp)
|
static boolean |
containsStatement(ProgramElement toSearchIn,
SourceElement toSearch,
Services services)
Checks if the given
ProgramElement contains the given SourceElement . |
static boolean |
containsSymbolicExecutionLabel(Term term)
Checks if the
Term or one of its sub terms contains
a symbolic execution label. |
static IExecutionVariable[] |
createAllExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionConstraint[] |
createExecutionConstraints(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
IExecutionConstraint s. |
static IExecutionVariable[] |
createExecutionVariables(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
createExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
createExecutionVariables(IExecutionNode<?> node,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
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 |
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 |
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 |
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 . |
static NotationInfo |
createNotationInfo(IExecutionElement element)
Creates the
NotationInfo for the given IExecutionElement . |
static NotationInfo |
createNotationInfo(Node node)
Creates the
NotationInfo for the given Node . |
static NotationInfo |
createNotationInfo(Proof proof)
Creates the
NotationInfo for the given Proof . |
static Term |
createSelectTerm(IExecutionVariable variable)
Creates recursive a term which can be used to determine the value
of
#getProgramVariable() . |
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term newSuccedent)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static boolean |
equalsWithPosition(SourceElement first,
SourceElement second)
Compares the given
SourceElement s including their PositionInfo s. |
static IProgramVariable |
extractExceptionVariable(Proof proof)
Extracts the exception variable which is used to check if the executed program in proof terminates normally.
|
protected static ImmutableArray<Term> |
extractValueFromUpdate(Term term,
IProgramVariable variable)
Utility method to extract the value of the
IProgramVariable
from the given update term. |
static Node |
findMethodCallNode(Node node,
PosInOccurrence pio)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp) ). |
static PosInOccurrence |
findModalityWithMaxSymbolicExecutionLabelId(Semisequent semisequent,
boolean inAntec)
Searches the modality
Term with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Semisequent . |
static PosInOccurrence |
findModalityWithMaxSymbolicExecutionLabelId(Sequent sequent)
Searches the modality
PosInOccurrence with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Sequent . |
static PosInTerm |
findModalityWithMaxSymbolicExecutionLabelId(Term term)
Searches the modality
PosInTerm with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Term . |
static PosInOccurrence |
findModalityWithMinSymbolicExecutionLabelId(Semisequent semisequent,
boolean inAntec)
Searches the modality
PosInOccurrence with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Semisequent . |
static PosInOccurrence |
findModalityWithMinSymbolicExecutionLabelId(Sequent sequent)
Searches the modality
PosInOccurrence with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Sequent . |
static PosInTerm |
findModalityWithMinSymbolicExecutionLabelId(Term term)
Searches the modality
PosInTerm with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Term . |
static Node |
findParentSetNode(Node node)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp) ). |
static IProgramVariable |
findSelfTerm(Node node,
PosInOccurrence pio)
|
static Term |
followPosInOccurrence(PosInOccurrence posInOccurrence,
Term term)
Returns the sub
Term at the given PosInOccurrence
but on the given Term instead of the one contained in the PosInOccurrence . |
static java.lang.String |
formatTerm(Term term,
Services services,
boolean useUnicode,
boolean usePrettyPrinting)
|
static Term |
getArrayIndex(Services services,
HeapLDT heapLDT,
Term arrayIndexTerm)
Returns the array index defined by the given
Term . |
static java.lang.String |
getChoiceSetting(java.lang.String key)
Returns the default choice value.
|
static java.util.HashMap<java.lang.String,java.lang.String> |
getDefaultTacletOptions()
Returns the default taclet options for symbolic execution.
|
static java.lang.String |
getDisplayString(IProgramVariable pv)
Returns the human readable name of the given
IProgramVariable . |
static ProgramVariable |
getProgramVariable(Services services,
HeapLDT heapLDT,
Term locationTerm)
Returns the
ProgramVariable defined by the given Term . |
static java.util.Set<IProgramVariable> |
getProgramVariables(FieldDeclaration fd)
Collects all
IProgramVariable s of the given FieldDeclaration . |
static IExecutionNode<?> |
getRoot(IExecutionNode<?> executionNode)
Returns the root of the given
IExecutionNode . |
static java.lang.String |
getSourcePath(PositionInfo posInfo)
Returns the path to the source file defined by the given
PositionInfo . |
static SymbolicExecutionTermLabel |
getSymbolicExecutionLabel(RuleApp ruleApp)
Returns the contained
SymbolicExecutionTermLabel if available. |
static SymbolicExecutionTermLabel |
getSymbolicExecutionLabel(Term term)
Returns the contained
SymbolicExecutionTermLabel if available. |
static boolean |
hasApplicableRules(Goal goal)
Checks if the
Goal has applicable rules. |
static boolean |
hasLoopBodyLabel(RuleApp ruleApp)
|
static boolean |
hasLoopBodyTerminationLabel(RuleApp ruleApp)
|
static boolean |
hasLoopCondition(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given
Node has a loop condition. |
static boolean |
hasReferenceSort(Services services,
IProgramVariable var)
Checks if the
Sort of the given IProgramVariable is a reference type. |
static boolean |
hasReferenceSort(Services services,
Sort sort)
Checks if the
Sort is a reference type. |
static boolean |
hasReferenceSort(Services services,
Term term)
|
static boolean |
hasSymbolicExecutionLabel(RuleApp ruleApp)
|
static boolean |
hasSymbolicExecutionLabel(Term term)
Checks if the given
Term contains a SymbolicExecutionTermLabel . |
static Term |
improveReadability(Term term,
Services services)
Improves the
Term to increase its readability. |
static void |
initializeStrategy(SymbolicExecutionTreeBuilder builder)
Initializes the
Proof of the given SymbolicExecutionTreeBuilder
so that the correct Strategy is used. |
static Term |
instantiateTerm(Node node,
Term term,
TacletApp tacletApp,
Services services)
|
static boolean |
isBaseHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is the base heap. |
static boolean |
isBlockContractValidityBranch(PosInOccurrence pio)
Checks if the modality at the given
PosInOccurrence represents the validity branch of an applied block contract. |
static boolean |
isBlockContractValidityBranch(RuleApp appliedRuleApp)
Checks if the modality at the applied rule represents the validity branch of an applied block contract.
|
static boolean |
isBlockSpecificationElement(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as block/loop contract.
|
static boolean |
isBoolean(Services services,
Operator op)
Checks if the given
Operator is a boolean. |
static boolean |
isBranchStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as branch statement.
|
static boolean |
isChoiceSettingInitialised()
Checks if the choice settings are initialized.
|
static boolean |
isCloseAfterJoin(RuleApp ruleApp)
Checks if the
CloseAfterMergeRuleBuiltInRuleApp is applied. |
static boolean |
isDoWhileLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a do while loop. |
static boolean |
isExceptionalMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as exceptional method return.
|
static boolean |
isForLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a for loop. |
static boolean |
isHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is a heap. |
static boolean |
isHeapUpdate(Services services,
Term term)
Checks if the given
Term represents a heap update,
in particular a store or create operation on a heap. |
static boolean |
isInImplicitMethod(Node node,
RuleApp ruleApp)
Checks if the currently executed code is in an implicit method
(
IProgramMethod.isImplicit() is true ). |
static boolean |
isJoin(RuleApp ruleApp)
Checks if the
MergeRuleBuiltInRuleApp is applied. |
static boolean |
isLoopBodyTermination(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop body termination.
|
static boolean |
isLoopInvariant(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop invariant.
|
static boolean |
isLoopStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as loop statement.
|
static boolean |
isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given node should be represented as method call.
|
static boolean |
isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement,
boolean allowImpliciteMethods)
Checks if the given node should be represented as method call.
|
static boolean |
isMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as method return.
|
static boolean |
isNotImplicit(Services services,
IProgramMethod pm)
Checks if the given
IProgramMethod is not implicit. |
static boolean |
isNotNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static boolean |
isNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static boolean |
isNullSort(Sort sort,
Services services)
|
static boolean |
isNumber(Operator op)
Checks if the given
Operator is a number. |
static boolean |
isOperationContract(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as operation contract.
|
static boolean |
isRuleAppToIgnore(RuleApp ruleApp)
Checks if the given
RuleApp should be ignored or
checked for possible symbolic execution tree node representation. |
static boolean |
isSelect(Services services,
Term term)
Checks if the given
Term is a select on a heap. |
static boolean |
isSkolemConstant(Term term)
|
static boolean |
isStatementNode(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as statement.
|
static boolean |
isStaticVariable(IProgramVariable programVariable)
Checks if the given
IProgramVariable is static or not. |
static boolean |
isSymbolicExecutionTreeNode(Node node,
RuleApp ruleApp)
|
static boolean |
isTerminationNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as termination.
|
static boolean |
isUsePrettyPrinting()
Checks if pretty printing is enabled or not.
|
static boolean |
isWeakeningGoalEnabled(Proof proof)
Checks if the weakening goal is enabled or not.
|
protected static Sequent |
labelSkolemConstants(Sequent sequent,
java.util.Set<Term> constantsToLabel,
TermFactory factory)
Labels all specified skolem equalities with the
RESULT_LABEL . |
static Sort |
lazyComputeExceptionSort(Node node,
IProgramVariable exceptionVariable)
Computes the exception
Sort lazily when #getExceptionSort()
is called the first time. |
static boolean |
lazyComputeIsAdditionalBranchVerified(Node node)
Checks if this branch would be closed without the uninterpreted predicate
and thus be treated as valid/closed in a regular proof.
|
static boolean |
lazyComputeIsExceptionalTermination(Node node,
IProgramVariable exceptionVariable)
Checks if is an exceptional termination.
|
static boolean |
lazyComputeIsMainBranchVerified(Node node)
Checks if this branch would be closed without the uninterpreted predicate
and thus be treated as valid/closed in a regular proof.
|
static ImmutableList<Term> |
listSemisequentTerms(Semisequent semisequent)
Lists the
Term s contained in the given Semisequent . |
static Term |
posInOccurrenceInOtherNode(Node original,
PosInOccurrence pio,
Node toApplyOn)
Returns the
Term described by the given PosInOccurrence of the original Node
in the Node to apply on. |
static Term |
posInOccurrenceInOtherNode(Sequent original,
PosInOccurrence pio,
Sequent toApplyOn)
Returns the
Term described by the given PosInOccurrence of the original Sequent
in the Sequent to apply on. |
static PosInOccurrence |
posInOccurrenceToOtherSequent(Node original,
PosInOccurrence pio,
Node toApplyTo)
Returns the
PosInOccurrence described by the given PosInOccurrence of the original Node
in the Node to apply too. |
static PosInOccurrence |
posInOccurrenceToOtherSequent(Sequent original,
PosInOccurrence pio,
Sequent toApplyTo)
Returns the
PosInOccurrence described by the given PosInOccurrence of the original Sequent
in the Sequent to apply too. |
static Term |
removeLabelRecursive(TermFactory tf,
Term term,
TermLabel label)
|
static Term |
replaceSkolemConstants(Sequent sequent,
Term term,
Services services)
Replaces all skolem constants in the given
Term . |
static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult |
searchContractPostOrExcPostExceptionVariable(Node node,
Services services)
Searches the used exception variable in the post or exceptional post branch of an applied
ContractRuleApp on the parent of the given Node . |
static Term |
sequentToImplication(Sequent sequent,
Services services)
Converts the given
Sequent into an implication. |
static void |
setChoiceSetting(java.lang.String key,
java.lang.String value)
Sets the default choice value.
|
static void |
setUsePrettyPrinting(boolean usePrettyPrinting)
Defines if pretty printing is enabled or not.
|
static Term |
simplify(InitConfig initConfig,
Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
simplify(InitConfig initConfig,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
simplify(Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static void |
updateStrategySettings(Proof proof,
boolean useOperationContracts,
boolean useLoopInvariants,
boolean nonExecutionBranchHidingSideProofs,
boolean aliasChecksImmediately)
Configures the proof to use the given settings.
|
static void |
updateStrategySettings(Proof proof,
StrategyProperties sp)
Configures the proof to use the given
StrategyProperties . |
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_BAN
public static final java.lang.String CHOICE_SETTING_RUNTIME_EXCEPTIONS_VALUE_ALLOW
public static final Name RESULT_LABEL_NAME
RESULT_LABEL
.public static final TermLabel RESULT_LABEL
Term
to evaluate in a side proof.public static final Name LOOP_BODY_LABEL_NAME
LOOP_BODY_LABEL
.public static final TermLabel LOOP_BODY_LABEL
public static final Name LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME
LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
.public static final TermLabel LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
public static Term simplify(InitConfig initConfig, Term term) throws ProofInputException
Term
in a side proof.initConfig
- The InitConfig
to use.term
- The Term
to simplify.Term
.ProofInputException
- Occurred Exception.public static Term simplify(Proof parentProof, Term term) throws ProofInputException
Term
in a side proof.parentProof
- The parent Proof
.term
- The Term
to simplify.Term
.ProofInputException
- Occurred Exception.public static Term simplify(InitConfig initConfig, Proof parentProof, Term term) throws ProofInputException
Term
in a side proof.initConfig
- The InitConfig
to use.parentProof
- The parent Proof
which provides the StrategySettings
.term
- The Term
to simplify.Term
.ProofInputException
- Occurred Exception.public static Term sequentToImplication(Sequent sequent, Services services)
Sequent
into an implication.public static ImmutableList<Term> listSemisequentTerms(Semisequent semisequent)
Term
s contained in the given Semisequent
.semisequent
- The Semisequent
to list terms of.Term
s.public static Term improveReadability(Term term, Services services)
Term
to increase its readability.
The following changes will be performed:
a < 1 + b
=> a <= b
a < b + 1
=> a <= b
a >= 1 + b
=> a > b
a >= b + 1
=> a > b
a <= -1 + b
=> a < b
a <= b + -1
=> a < b
a <= b - 1
=> a < b
a > -1 + b
=> a >= b
a > b + -1
=> a >= b
a > b - 1
=> a >= b
a >= 1 + b
=> a > b
a >= b + 1
=> a > b
!a >= b
=> a < b
!a > b
=> a <= b
!a <= b
=> a > b
!a < b
=> a >= b
public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractReturnVariableValueSequent(Services services, TypeReference contextObjectType, IProgramMethod contextMethod, ReferencePrefix contextObject, Node methodReturnNode, Node methodCallEmptyNode, IProgramVariable variable)
Sequent
which can be used in site proofs to
extract the return value of the given IProgramVariable
from the
sequent of the given Node
.services
- The Services
to use.contextObjectType
- The type of the current object (this reference).contextMethod
- The current method.contextObject
- The current object (this reference).methodReturnNode
- The method return Node
which provides the sequent to extract updates and return expression from.methodCallEmptyNode
- The method call empty Node
which provides the sequent to start site proof in.variable
- The IProgramVariable
of the value which is interested.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractReturnVariableValueSequent(Services services, IExecutionContext context, Node methodReturnNode, Node methodCallEmptyNode, IProgramVariable variable)
Sequent
which can be used in site proofs to
extract the return value of the given IProgramVariable
from the
sequent of the given Node
.services
- The Services
to use.context
- The IExecutionContext
that defines the current object (this reference).methodReturnNode
- The method return Node
which provides the sequent to extract updates and return expression from.methodCallEmptyNode
- The method call empty Node
which provides the sequent to start site proof in.variable
- The IProgramVariable
of the value which is interested.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractVariableValueSequent(Services services, Node node, PosInOccurrence pio, Term additionalConditions, IProgramVariable variable)
Sequent
which can be used in site proofs to
extract the value of the given IProgramVariable
from the
sequent of the given Node
.services
- The Services
to use.node
- The original Node
which provides the sequent to extract from.pio
- The PosInOccurrence
of the SE modality.additionalConditions
- Optional additional conditions.variable
- The IProgramVariable
of the value which is interested.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static SymbolicExecutionUtil.SiteProofVariableValueInput createExtractTermSequent(Services sideProofServices, Node node, PosInOccurrence pio, Term additionalConditions, Term term, boolean keepUpdates)
Sequent
which can be used in site proofs to
extract the value of the given IProgramVariable
from the
sequent of the given Node
.sideProofServices
- The Services
of the side proof to use.node
- The original Node
which provides the sequent to extract from.pio
- The PosInOccurrence
of the modality or its updates.additionalConditions
- Additional conditions to add to the antecedent.term
- The new succedent term.keepUpdates
- true
keep updates, false
throw updates away.SymbolicExecutionUtil.SiteProofVariableValueInput
with the created sequent and the predicate which will contain the value.public static boolean isHeapUpdate(Services services, Term term)
Term
represents a heap update,
in particular a store or create operation on a heap.public static boolean canComputeVariables(IExecutionNode<?> node, Services services) throws ProofInputException
IExecutionNode
via IExecutionNode.getVariables()
.node
- The IExecutionNode
to check.services
- The Services
to use.true
right now it is possible to compute variables, false
it is not possible to compute variables.ProofInputException
- Occurred Exception.public static IExecutionConstraint[] createExecutionConstraints(IExecutionNode<?> node)
IExecutionNode
the contained
IExecutionConstraint
s.node
- The IExecutionNode
to create constraints for.IExecutionConstraint
s.public static boolean containsSymbolicExecutionLabel(Term term)
Term
or one of its sub terms contains
a symbolic execution label.term
- The Term
to check.true
SE label is somewhere contained, false
SE label is not contained at all.public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node) throws ProofInputException
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.IExecutionVariable
s.ProofInputException
public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node, Term condition) throws ProofInputException
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.condition
- A Term
specifying some additional constraints to consider.IExecutionVariable
s.ProofInputException
public static IExecutionVariable[] createExecutionVariables(IExecutionNode<?> node, Node proofNode, PosInOccurrence modalityPIO, Term condition) throws ProofInputException
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.proofNode
- The proof Node
to work with.modalityPIO
- The PosInOccurrence
of the modality of interest.condition
- A Term
specifying some additional constraints to consider.IExecutionVariable
s.ProofInputException
public static IExecutionVariable[] createAllExecutionVariables(IExecutionNode<?> node, Node proofNode, PosInOccurrence modalityPIO, Term condition)
IExecutionNode
the contained
root IExecutionVariable
s.node
- The IExecutionNode
to create variables for.proofNode
- The proof Node
to work with.modalityPIO
- The PosInOccurrence
of the modality of interest.condition
- A Term
specifying some additional constraints to consider.IExecutionVariable
s.public static java.util.List<IProgramVariable> collectAllElementaryUpdateTerms(Node node)
IProgramVariable
used in ElementaryUpdate
s.node
- The Node
to search in.IProgramVariable
which are used in ElementaryUpdate
s.public static ProgramVariable getProgramVariable(Services services, HeapLDT heapLDT, Term locationTerm)
ProgramVariable
defined by the given Term
.services
- The Services
to use.heapLDT
- The HeapLDT
to use.locationTerm
- The Term
to extract ProgramVariable
from.Term
s ProgramVariable
or null
if not available.public static Term getArrayIndex(Services services, HeapLDT heapLDT, Term arrayIndexTerm)
Term
.public static IProgramVariable findSelfTerm(Node node, PosInOccurrence pio)
node
- The Node
to search in.pio
- The PosInOccurrence
describing the location of the modality of interest.IProgramVariable
with the current this
/self
reference or null
if no one is available.public static boolean isMethodCallNode(Node node, RuleApp ruleApp, SourceElement statement)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).true
represent node as method call, false
represent node as something else.public static boolean isMethodCallNode(Node node, RuleApp ruleApp, SourceElement statement, boolean allowImpliciteMethods)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).allowImpliciteMethods
- true
implicit methods are included, false
implicit methods are outfiltered.true
represent node as method call, false
represent node as something else.public static boolean isNotImplicit(Services services, IProgramMethod pm)
IProgramMethod
is not implicit.services
- The Services
to use.pm
- The IProgramMethod
to check.true
is not implicit, false
is implicitpublic static boolean isBranchStatement(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).posInfo
- The PositionInfo
.true
represent node as branch statement, false
represent node as something else.public static boolean isLoopStatement(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).posInfo
- The PositionInfo
.true
represent node as loop statement, false
represent node as something else.public static boolean isStatementNode(Node node, RuleApp ruleApp, SourceElement statement, PositionInfo posInfo)
node
- The current Node
in the proof tree of KeY.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The statement (SourceElement
).posInfo
- The PositionInfo
.true
represent node as statement, false
represent node as something else.public static boolean isTerminationNode(Node node, RuleApp ruleApp)
public static boolean isOperationContract(Node node, RuleApp ruleApp)
public static boolean isBlockSpecificationElement(Node node, RuleApp ruleApp)
public static boolean isLoopInvariant(Node node, RuleApp ruleApp)
public static boolean isMethodReturnNode(Node node, RuleApp ruleApp)
public static boolean isExceptionalMethodReturnNode(Node node, RuleApp ruleApp)
public static boolean hasLoopCondition(Node node, RuleApp ruleApp, SourceElement statement)
Node
has a loop condition.node
- The Node
to check.ruleApp
- The RuleApp
may used or not used in the rule.statement
- The actual statement (SourceElement
).true
has loop condition, false
has no loop condition.public static boolean hasLoopBodyLabel(RuleApp ruleApp)
ruleApp
- The RuleApp
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given RuleApp
is null
.public static boolean hasLoopBodyTerminationLabel(RuleApp ruleApp)
ruleApp
- The RuleApp
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given RuleApp
is null
.public static boolean hasSymbolicExecutionLabel(RuleApp ruleApp)
ruleApp
- The RuleApp
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given RuleApp
is null
.public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(RuleApp ruleApp)
SymbolicExecutionTermLabel
if available.ruleApp
- The RuleApp
may used or not used in the rule.SymbolicExecutionTermLabel
or null
if no SymbolicExecutionTermLabel
is provided.public static boolean hasSymbolicExecutionLabel(Term term)
Term
contains a SymbolicExecutionTermLabel
.term
- The Term
to check.true
contains a SymbolicExecutionTermLabel
, false
does not contain a SymbolicExecutionTermLabel
or the given Term
is null
.public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(Term term)
SymbolicExecutionTermLabel
if available.term
- The Term
to search in.SymbolicExecutionTermLabel
or null
if no SymbolicExecutionTermLabel
is provided.public static PosInOccurrence findModalityWithMaxSymbolicExecutionLabelId(Sequent sequent)
PosInOccurrence
with the maximal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Sequent
.sequent
- The Sequent
to search in.PosInOccurrence
with the maximal ID if available or null
otherwise.public static PosInOccurrence findModalityWithMaxSymbolicExecutionLabelId(Semisequent semisequent, boolean inAntec)
Term
with the maximal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Semisequent
.semisequent
- The Semisequent
to search in.inAntec
- true
antecedent, false
succedent.Term
with the maximal ID if available or null
otherwise.public static PosInTerm findModalityWithMaxSymbolicExecutionLabelId(Term term)
PosInTerm
with the maximal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Term
.public static PosInOccurrence findModalityWithMinSymbolicExecutionLabelId(Sequent sequent)
PosInOccurrence
with the minimal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Sequent
.sequent
- The Sequent
to search in.PosInOccurrence
with the maximal ID if available or null
otherwise.public static PosInOccurrence findModalityWithMinSymbolicExecutionLabelId(Semisequent semisequent, boolean inAntec)
PosInOccurrence
with the minimal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Semisequent
.semisequent
- The Semisequent
to search in.inAntec
- true
antecedent, false
succedent.PosInOccurrence
with the minimal ID if available or null
otherwise.public static PosInTerm findModalityWithMinSymbolicExecutionLabelId(Term term)
PosInTerm
with the minimal SymbolicExecutionTermLabel
ID
SymbolicExecutionTermLabel.getId()
in the given Term
.public static boolean isSymbolicExecutionTreeNode(Node node, RuleApp ruleApp)
public static boolean isRuleAppToIgnore(RuleApp ruleApp)
RuleApp
should be ignored or
checked for possible symbolic execution tree node representation.public static boolean isInImplicitMethod(Node node, RuleApp ruleApp)
IProgramMethod.isImplicit()
is true
).public static int computeStackSize(RuleApp ruleApp)
public static boolean isDoWhileLoopCondition(Node node, SourceElement statement)
SourceElement
is a do while loop.node
- The Node
to check.statement
- The actual statement (SourceElement
).true
is do while loop, false
is something else.public static boolean isForLoopCondition(Node node, SourceElement statement)
SourceElement
is a for loop.node
- The Node
to check.statement
- The actual statement (SourceElement
).true
is for loop, false
is something else.public static ImmutableList<Goal> collectGoalsInSubtree(IExecutionElement executionElement)
Goal
s in the subtree of the given IExecutionElement
.executionElement
- The IExecutionElement
to collect Goal
s in.Goal
s.public static ImmutableList<Goal> collectGoalsInSubtree(Node node)
public static Node findMethodCallNode(Node node, PosInOccurrence pio)
Node
the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp)
).node
- The Node
to start search in.pio
- The PosInOccurrence
of the modality.Node
of the given Node
which is also a set node or null
if no parent node was found.public static Node findParentSetNode(Node node)
Node
the parent node
which also represents a symbolic execution tree node
(checked via isSymbolicExecutionTreeNode(Node, RuleApp)
).public static Term computeBranchCondition(Node node, boolean simplify, boolean improveReadability) throws ProofInputException
Node
.node
- The Node
to compute its branch condition.simplify
- true
simplify condition in a side proof, false
do not simplify condition.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.public static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult searchContractPostOrExcPostExceptionVariable(Node node, Services services) throws ProofInputException
ContractRuleApp
on the parent of the given Node
.node
- The Node
which is the post or exceptional post branch of an applied ContractRuleApp
.services
- The Services
to use.ProofInputException
- Occurred exception if something is not as expected.public static Term posInOccurrenceInOtherNode(Node original, PosInOccurrence pio, Node toApplyOn)
Term
described by the given PosInOccurrence
of the original Node
in the Node
to apply on.original
- The original Node
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyOn
- The new Node
to apply the PosInOccurrence
on.Term
in the other Node
described by the PosInOccurrence
or null
if not available.public static Term posInOccurrenceInOtherNode(Sequent original, PosInOccurrence pio, Sequent toApplyOn)
Term
described by the given PosInOccurrence
of the original Sequent
in the Sequent
to apply on.original
- The original Sequent
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyOn
- The new Sequent
to apply the PosInOccurrence
on.Term
in the other Sequent
described by the PosInOccurrence
or null
if not available.public static PosInOccurrence posInOccurrenceToOtherSequent(Node original, PosInOccurrence pio, Node toApplyTo)
PosInOccurrence
described by the given PosInOccurrence
of the original Node
in the Node
to apply too.original
- The original Node
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyTo
- The new Node
to apply the PosInOccurrence
to.PosInOccurrence
in the other Node
described by the PosInOccurrence
or null
if not available.public static PosInOccurrence posInOccurrenceToOtherSequent(Sequent original, PosInOccurrence pio, Sequent toApplyTo)
PosInOccurrence
described by the given PosInOccurrence
of the original Sequent
in the Sequent
to apply too.original
- The original Sequent
on which the given PosInOccurrence
works.pio
- The given PosInOccurrence
.toApplyTo
- The new Sequent
to apply the PosInOccurrence
to.PosInOccurrence
in the other Sequent
described by the PosInOccurrence
or null
if not available.public static Term followPosInOccurrence(PosInOccurrence posInOccurrence, Term term)
Term
at the given PosInOccurrence
but on the given Term
instead of the one contained in the PosInOccurrence
.posInOccurrence
- The PosInOccurrence
which defines the sub term position.term
- The Term
to work with.Term
or null
if the PosInOccurrence
is not compatible.public static Term instantiateTerm(Node node, Term term, TacletApp tacletApp, Services services)
public static java.lang.String getChoiceSetting(java.lang.String key)
null
if it is called before
a proof is instantiated the first time. It can be checked via
isChoiceSettingInitialised()
.key
- The choice key.public static void setChoiceSetting(java.lang.String key, java.lang.String value)
isChoiceSettingInitialised()
.key
- The choice key to modify.value
- The new choice value to set.public static boolean isNull(Node node, Term additionalAntecedent, Term newSuccedent) throws ProofInputException
public static boolean isNotNull(Node node, Term additionalAntecedent, Term newSuccedent) throws ProofInputException
public static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term newSuccedent)
public static Sequent createSequentToProveWithNewSuccedent(Node node, Term additionalAntecedent, Term newSuccedent, boolean addResultLabel)
public static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term additionalAntecedent, Term newSuccedent, boolean addResultLabel)
public static ImmutableList<Term> computeRootElementaryUpdates(Node root)
ElementaryUpdate
s on the given root Node
.root
- The root Node
of the Proof
.ElementaryUpdate
s.public static ImmutableList<Term> collectElementaryUpdates(Term term)
ElementaryUpdate
s in the given Term
.term
- The Term
to collect its updates.ElementaryUpdate
s.public static Sequent createSequentToProveWithNewSuccedent(Node node, Term additionalAntecedent, Term newSuccedent, ImmutableList<Term> updates, boolean addResultLabel)
public static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccurrence pio, Term additionalAntecedent, Term newSuccedent, ImmutableList<Term> updates, boolean addResultLabel)
protected static Sequent labelSkolemConstants(Sequent sequent, java.util.Set<Term> constantsToLabel, TermFactory factory)
RESULT_LABEL
.sequent
- The Sequent
to modify.constantsToLabel
- The skolem constants to label.factory
- The TermFactory
to use.Sequent
.public static Term removeLabelRecursive(TermFactory tf, Term term, TermLabel label)
tf
- The TermFactory
to use.term
- The Term
to remove label from.label
- The TermLabel
to remove.Term
without the given TermLabel
.public static boolean isSkolemConstant(Term term)
public static int checkSkolemEquality(SequentFormula sf)
SequentFormula
is a skolem equality.sf
- The SequentFormula
to check.-1
left side of skolem equality, 0
no skolem equality, 1
right side of skolem equality.public static int checkSkolemEquality(Term term)
Term
is a skolem equality.sf
- The Term
to check.-1
left side of skolem equality, 0
no skolem equality, 1
right side of skolem equality.public static Term replaceSkolemConstants(Sequent sequent, Term term, Services services)
Term
.public static boolean isStaticVariable(IProgramVariable programVariable)
IProgramVariable
is static or not.true
is static, false
is not static or is array cell.public static java.util.Set<IProgramVariable> getProgramVariables(FieldDeclaration fd)
IProgramVariable
s of the given FieldDeclaration
.fd
- The given FieldDeclaration
.IProgramVariable
s for the given FieldDeclaration
.public static Term computePathCondition(Node node, boolean simplify, boolean improveReadability) throws ProofInputException
Node
.node
- The Node
to compute its path condition.simplify
- true
simplify each branch condition in a side proof, false
do not simplify branch conditions.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.public static Term computePathCondition(Node parentNode, Node childNode, boolean simplify, boolean improveReadability) throws ProofInputException
Node
s.parentNode
- The Node
to stop path condition computation at.childNode
- The Node
to compute its path condition back to the parent.simplify
- true
simplify each branch condition in a side proof, false
do not simplify branch conditions.improveReadability
- true
improve readability, false
do not improve readability.ProofInputException
- Occurred Exception.public static boolean hasReferenceSort(Services services, IProgramVariable var)
Sort
of the given IProgramVariable
is a reference type.services
- The Services
to use.var
- The IProgramVariable
to check.true
is reference sort, false
is no reference sort.public static boolean hasReferenceSort(Services services, Sort sort)
Sort
is a reference type.public static java.lang.String getDisplayString(IProgramVariable pv)
IProgramVariable
.pv
- The IProgramVariable
to get its name.IProgramVariable
.public static IExecutionNode<?> getRoot(IExecutionNode<?> executionNode)
IExecutionNode
.executionNode
- The IExecutionNode
to get the root of its symbolic execution tree.IExecutionNode
.public static IProgramVariable extractExceptionVariable(Proof proof)
proof
- The Proof
to extract variable from.public static void updateStrategySettings(Proof proof, boolean useOperationContracts, boolean useLoopInvariants, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecksImmediately)
proof
- The Proof
to configure.useOperationContracts
- true
use operation contracts, false
expand methods.useLoopInvariants
- true
use loop invariants, false
expand loops.nonExecutionBranchHidingSideProofs
- true
hide non execution branch labels by side proofs, false
do not hide execution branch labels.useLoopInvariants
- true
immediately alias checks, false
alias checks never.public static void updateStrategySettings(Proof proof, StrategyProperties sp)
StrategyProperties
.proof
- The Proof
to configure.sb
- The StrategyProperties
to set.public static boolean isChoiceSettingInitialised()
true
settings are initialized, false
settings are not initialized.public static boolean isLoopBodyTermination(Node node, RuleApp ruleApp)
public static boolean isHeap(Operator op, HeapLDT heapLDT)
Operator
is a heap.public static boolean isBaseHeap(Operator op, HeapLDT heapLDT)
Operator
is the base heap.public static java.lang.String getSourcePath(PositionInfo posInfo)
PositionInfo
.posInfo
- The PositionInfo
to extract source file from.null
if not available.public static boolean isSelect(Services services, Term term)
Term
is a select on a heap.public static boolean isNumber(Operator op)
Operator
is a number.op
- The Operator
to check.true
is number, false
is something else.public static boolean isBoolean(Services services, Operator op)
Operator
is a boolean.op
- The Operator
to check.true
is boolean, false
is something else.public static java.util.HashMap<java.lang.String,java.lang.String> getDefaultTacletOptions()
public static java.lang.String formatTerm(Term term, Services services, boolean useUnicode, boolean usePrettyPrinting)
Converts the given Term
into a String
respecting #isUsePretty()
.
The functionality is similar to OutputStreamProofSaver.printTerm(Term, Services, boolean)
but allows to set custom settings.
public static boolean isUsePrettyPrinting()
true
pretty printing is enabled, false
pretty printing is disabled.public static void setUsePrettyPrinting(boolean usePrettyPrinting)
usePrettyPrinting
- true
pretty printing is enabled, false
pretty printing is disabled.public static boolean hasApplicableRules(Goal goal)
Goal
has applicable rules.goal
- The Goal
to check.true
has applicable rules, false
no rules are applicable.public static Pair<java.lang.Integer,SourceElement> computeSecondStatement(RuleApp ruleApp)
NodeInfo.computeActiveStatement(SourceElement)
.ruleApp
- The RuleApp
.public static boolean equalsWithPosition(SourceElement first, SourceElement second)
SourceElement
s including their PositionInfo
s.first
- The first SourceElement
.second
- The second SourceElement
.true
both are equal and at the same PositionInfo
, false
otherwise.public static boolean containsStatement(ProgramElement toSearchIn, SourceElement toSearch, Services services)
ProgramElement
contains the given SourceElement
.toSearchIn
- The ProgramElement
to search in.toSearch
- The SourceElement
to search.services
- The Services
to use.true
contained, false
not contained.public static Term createSelectTerm(IExecutionVariable variable)
#getProgramVariable()
.services
- The Services
to use.public static NotationInfo createNotationInfo(IExecutionElement element)
NotationInfo
for the given IExecutionElement
.element
- The IExecutionElement
to create its NotationInfo
.NotationInfo
.public static NotationInfo createNotationInfo(Node node)
NotationInfo
for the given Node
.node
- The Node
to create its NotationInfo
.NotationInfo
.public static NotationInfo createNotationInfo(Proof proof)
NotationInfo
for the given Proof
.proof
- The Proof
to create its NotationInfo
.NotationInfo
.public static boolean lazyComputeIsMainBranchVerified(Node node)
true
verified/closed, false
not verified/still openpublic static boolean lazyComputeIsAdditionalBranchVerified(Node node)
true
verified/closed, false
not verified/still openpublic static boolean lazyComputeIsExceptionalTermination(Node node, IProgramVariable exceptionVariable)
node
- the node which is used for computation.exceptionVariable
- the exception variable which is used to check if the executed program in proof terminates normally.true
exceptional termination, false
normal termination.public static Sort lazyComputeExceptionSort(Node node, IProgramVariable exceptionVariable)
Sort
lazily when #getExceptionSort()
is called the first time.node
- the node which is user for computation.exceptionVariable
- the exception variable which is used to check if the executed program in proof terminates normally.Sort
.protected static ImmutableArray<Term> extractValueFromUpdate(Term term, IProgramVariable variable)
IProgramVariable
from the given update term.term
- The given update term.variable
- The IProgramVariable
for that the value is needed.null
if it is not defined in the given update term.public static void initializeStrategy(SymbolicExecutionTreeBuilder builder)
Proof
of the given SymbolicExecutionTreeBuilder
so that the correct Strategy
is used.builder
- The SymbolicExecutionTreeBuilder
to initialize.public static boolean isBlockContractValidityBranch(RuleApp appliedRuleApp)
appliedRuleApp
- The RuleApp
to check.true
validitiy branch, false
otherwise.public static boolean isBlockContractValidityBranch(PosInOccurrence pio)
PosInOccurrence
represents the validity branch of an applied block contract.pio
- The PosInOccurrence
to check.false
otherwise.public static boolean isJoin(RuleApp ruleApp)
MergeRuleBuiltInRuleApp
is applied.ruleApp
- The RuleApp
to check.true
is MergeRuleBuiltInRuleApp
, false
otherwise.public static boolean isCloseAfterJoin(RuleApp ruleApp)
CloseAfterMergeRuleBuiltInRuleApp
is applied.ruleApp
- The RuleApp
to check.true
is CloseAfterMergeRuleBuiltInRuleApp
, false
otherwise.Copyright © 2003-2019 The KeY-Project.