Closed danglotb closed 6 years ago
Sorry for the double post.
But I am on a work around.
I extended the StateFormatterText
and override the method formatState(State state)
with:
@Override
public void formatState(State state) {
super.formatState(state);
this.states.add(state);
}
Where states, is a static List
of State
, which allows the use to do:
p.setStateFormatMode(RunParameters.StateFormatMode.FULLTEXTHISTORY);
final Run r = new Run(p);
r.run();
final List<State> states = StateFormatterTextWithHistory.getStates();
I know this is an ugly solution, but it is the quickest that I found.
What do you think?
Best,
-- Benjamin.
Hi Benjamin, and sorry again for this late answer. I would not use this solution for two reasons. First, if you save all the states in a history as you did you will not obtain what you want, because the states in JBSE are mutable. To avoid wasting too many resources, the execution of a bytecode picks the pre-state, modifies it, and makes it the post-state. If you want to preserve a state you must clone it, so if you really really want to store the whole history of the execution you must change your second line in the formatState
method as follows:
this.states.add(state.clone());
but, here it comes the second reason, this way you will end up consuming a lot of memory. I don't believe you will be able to store the whole history of a program with more than a few states, unless the program is very simple. If possible work on-the-fly: do not store histories but elaborate the single states and then discard them. To answer to your initial question, it seems to me that you want the path condition at the final state of the execution. Since in general you have many final states each with its path condition, your code should be something like:
...
r.run();
Result result = r.getResult();
//iterate through all the path conditions of all the end states
for (State s : result.states()) {
...s.getPathCondition()... //do something with the path condition, typically iterate through its clauses
}
You can easily implement this as follows (this is just a hint, I have not compiled the code that follows):
public class Result {
private ArrayList<State> states = new ArrayList<>()
public void addState(State s) { this.states.add(s); }
public ArrayList<State> states() { return this.states; }
}
and modify the class jbse.apps.Run
as follows:
public final class Run {
private Result result = new Result(); //added
public Result getResult() { return this.result; } //added
...
private class ActionsRun extends Runner.Actions {
...
public boolean atTraceEnd() {
try {
final State currentState = Run.this.engine.getCurrentState();
Run.this.result.addState(currentState.clone()); //added
...
}
...
}
...
}
...
}
Best, Pietro
Hi,
I would like to have information contained in the PathCondition clause (in the ouput when using the
FULLTEXT
StateShowMode) programmatically.More precisely, I would like to do something like:
The object
Result
, accessible from theRun
object would contains the information contained intoPathCondition
, such as:I look on getters, to have this information, but I could not find anything.
After, I though to develop a
StateFormatMode
to output XML and then parse this XML to have the required information. But, I think it might be overkill to create a such object just to have this.You may have suggestions about this?
Do you have any guidelines to contribute? Do you have any tips regarding the development of a such Formatter?
I would be glad to contribute to JBSE.
Thank you very much.
-- Benjamin.