public class NodeInfo
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
void |
addRelevantFile(java.net.URI relevantFile)
Add a file to the set returned by
getRelevantFiles() . |
void |
addRelevantFiles(ImmutableSet<java.net.URI> relevantFiles)
Add some files to the set returned by
getRelevantFiles() . |
static SourceElement |
computeActiveStatement(RuleApp ruleApp)
Computes the active statement in the given
RuleApp . |
static SourceElement |
computeActiveStatement(SourceElement firstStatement)
Computes the active statement in the given
SourceElement . |
static SourceElement |
computeFirstStatement(RuleApp ruleApp)
Computes the first statement in the given
RuleApp . |
SourceElement |
getActiveStatement()
returns the active statement of the JavaBlock the applied
rule has been matched against or null if no rule has been applied yet
or the applied rule was no taclet or program transformation rule
|
java.lang.String |
getBranchLabel()
returns the branch label
|
java.lang.String |
getExecStatementParentClass()
returns the name of the source file where the active statement
occurs or the string NONE if the statement does not originate from a
source file (e.g.
|
Position |
getExecStatementPosition()
returns the position of the executed statement in its source code
or Position.UNDEFINED
|
java.lang.String |
getFirstStatementString()
returns a string representation of the first statement or null if no such
exists
|
boolean |
getInteractiveRuleApplication()
returns true if the rule applied on this node has been performed
manually by the user
|
java.lang.String |
getNotes()
Get user-provided plain-text annotations.
|
ImmutableSet<java.net.URI> |
getRelevantFiles()
Returns a set containing URIs of all files relevant to this node.
|
boolean |
getScriptRuleApplication()
returns true if the rule applied on this node has been performed
by a proof script command.
|
SequentChangeInfo |
getSequentChangeInfo() |
static boolean |
isSymbolicExecution(Taclet t) |
static boolean |
isSymbolicExecutionRuleApplied(Node node)
Checks if a rule is applied on the given
Node which performs symbolic execution. |
static boolean |
isSymbolicExecutionRuleApplied(RuleApp app)
Checks if the given
RuleApp performs symbolic execution. |
void |
setBranchLabel(java.lang.String s)
sets the branch label of a node.
|
void |
setInteractiveRuleApplication(boolean b)
parameter indicated if the rule has been applied interactively or
not
|
void |
setNotes(java.lang.String newNotes)
Add user-provided plain-text annotations.
|
void |
setScriptRuleApplication(boolean b)
parameter indicated if the rule has been applied by a proof script or not
|
void |
setSequentChangeInfo(SequentChangeInfo sequentChangeInfo) |
public NodeInfo(Node node)
public static SourceElement computeActiveStatement(RuleApp ruleApp)
Computes the active statement in the given RuleApp
.
This functionality is independent from concrete NodeInfo
s
and used for instance by the symbolic execution tree extraction.
ruleApp
- The given RuleApp
.null
if no one is provided.public static SourceElement computeFirstStatement(RuleApp ruleApp)
Computes the first statement in the given RuleApp
.
This functionality is independent from concrete NodeInfo
s
and used for instance by the symbolic execution tree extraction.
ruleApp
- The given RuleApp
.null
if no one is provided.public static SourceElement computeActiveStatement(SourceElement firstStatement)
Computes the active statement in the given SourceElement
.
This functionality is independent from concrete NodeInfo
s
and used for instance by the symbolic execution tree extraction.
firstStatement
- The given SourceElement
.null
if no one is provided.public static boolean isSymbolicExecutionRuleApplied(Node node)
Node
which performs symbolic execution.node
- The Node
to check.true
symbolic execution is performed, false
otherwise.public static boolean isSymbolicExecutionRuleApplied(RuleApp app)
RuleApp
performs symbolic execution.app
- The RuleApp
to check.true
symbolic execution is performed, false
otherwise.public static boolean isSymbolicExecution(Taclet t)
public SourceElement getActiveStatement()
public java.lang.String getBranchLabel()
public java.lang.String getExecStatementParentClass()
public Position getExecStatementPosition()
public java.lang.String getFirstStatementString()
public void setBranchLabel(java.lang.String s)
s
- the String to be setpublic void setInteractiveRuleApplication(boolean b)
b
- a boolean indicating interactive applicationpublic void setScriptRuleApplication(boolean b)
b
- a boolean indicating scripting applicationpublic boolean getInteractiveRuleApplication()
public boolean getScriptRuleApplication()
public ImmutableSet<java.net.URI> getRelevantFiles()
Returns a set containing URIs of all files relevant to this node.
This includes the files contained in the PositionInfo
of all modalities
as well as the files in the OriginTermLabel
s of all terms in this node's sequent.
public void addRelevantFile(java.net.URI relevantFile)
getRelevantFiles()
.relevantFile
- the URI of the file to add.public void addRelevantFiles(ImmutableSet<java.net.URI> relevantFiles)
getRelevantFiles()
.relevantFiles
- the URIs of the files to add.public void setNotes(java.lang.String newNotes)
newNotes
- annotations as described abovepublic java.lang.String getNotes()
public SequentChangeInfo getSequentChangeInfo()
public void setSequentChangeInfo(SequentChangeInfo sequentChangeInfo)
Copyright © 2003-2019 The KeY-Project.