public class NodeInfo
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private SourceElement |
activeStatement
firstStatement stripped of method frames
|
private java.lang.String |
branchLabel |
private boolean |
determinedFstAndActiveStatement
flag true if the first and active statement have been determined
|
private SourceElement |
firstStatement
used for proof tree annotation when applicable
|
private java.lang.String |
firstStatementString |
private boolean |
interactiveApplication
has the rule app of the node been applied interactively?
|
private Node |
node
the node this info object belongs to
|
private java.lang.String |
notes
User-provided plain-text annotations to the node.
|
private boolean |
scriptingApplication
has the rule app of the node been applied by a proof script?
|
private SequentChangeInfo |
sequentChangeInfo
Information about changes respective to the parent of this node.
|
private static java.util.Set<Name> |
symbolicExecNames |
Modifier and Type | Method and Description |
---|---|
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 . |
private void |
determineFirstAndActiveStatement()
determines the first and active statement if the applied
taclet worked on a modality
|
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. created by a taclet application or part of a
generated implicit method)
|
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.
|
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) |
(package private) void |
updateNoteInfo() |
private static java.util.Set<Name> symbolicExecNames
private SourceElement activeStatement
private java.lang.String branchLabel
private boolean determinedFstAndActiveStatement
private SourceElement firstStatement
private java.lang.String firstStatementString
private final Node node
private boolean interactiveApplication
private boolean scriptingApplication
private java.lang.String notes
private SequentChangeInfo sequentChangeInfo
public NodeInfo(Node node)
private void determineFirstAndActiveStatement()
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.void updateNoteInfo()
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 void setNotes(java.lang.String newNotes)
newNotes
- annotations as described abovepublic java.lang.String getNotes()
public SequentChangeInfo getSequentChangeInfo()
public void setSequentChangeInfo(SequentChangeInfo sequentChangeInfo)