Skip to content

Commit

Permalink
Fixed the error when Empty main runs with VerTracker (#494)
Browse files Browse the repository at this point in the history
  • Loading branch information
shreyasCs012 authored Aug 31, 2024
1 parent 3bda719 commit 7d2f7a9
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/main/gov/nasa/jpf/listener/VarTracker.java
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,9 @@ public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Inst
varId = ((JVMFieldInstruction)executedInsn).getFieldName();

StackFrame frame = ti.getModifiableTopFrame();
frame.addOperandAttr(varId);
if (frame.getTopPos() >= 0) {
frame.addOperandAttr(varId);
}


// here come the changes - note that we can't update the stats right away,
Expand Down
21 changes: 21 additions & 0 deletions src/tests/gov/nasa/jpf/listener/VerTrackerTest.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
package gov.nasa.jpf.listener;
import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;

class Emptymain{
public static void main(String[] args) {

}
}
public class VerTrackerTest extends TestJPF {
@Test
public void test_Emptymain(){
if(verifyNoPropertyViolation("+listener=gov.nasa.jpf.listener.VarTracker")){
Emptymain.main(null);
}
}
public static void main(String[] args) {
runTestsOfThisClass(null);
}

}

0 comments on commit 7d2f7a9

Please sign in to comment.