public class NodeInfo extends Object
Modifier and Type | Field and Description |
---|---|
private SourceElement |
activeStatement
firstStatement stripped of method frames
|
private 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 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 String |
notes
User-provided plain-text annotations to the node.
|
private static 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
|
String |
getBranchLabel()
returns the branch label
|
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
|
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
|
String |
getNotes()
Get user-provided plain-text annotations.
|
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(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(String newNotes)
Add user-provided plain-text annotations.
|
(package private) void |
updateNoteInfo() |
private SourceElement activeStatement
private String branchLabel
private boolean determinedFstAndActiveStatement
private SourceElement firstStatement
private String firstStatementString
private final Node node
private boolean interactiveApplication
private String notes
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.node
- The Node
to check.true
symbolic execution is performed, false
otherwise.public static boolean isSymbolicExecution(Taclet t)
public SourceElement getActiveStatement()
public String getBranchLabel()
public String getExecStatementParentClass()
public Position getExecStatementPosition()
public String getFirstStatementString()
public void setBranchLabel(String s)
s
- the String to be setpublic void setInteractiveRuleApplication(boolean b)
b
- a boolean indicating interactive applicationpublic boolean getInteractiveRuleApplication()
public void setNotes(String newNotes)
public String getNotes()