From: Seyed Amir Hossein Aqajari <saqajari@circinus-5.ics.uci.edu>
Date: Thu, 13 Feb 2020 21:39:36 +0000 (-0800)
Subject: JPF ready to run with old infrastructure
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=9ccd91c977cd17b3db4030e84af883ffb6b7c351

JPF ready to run with old infrastructure
---

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 3ec1eea..fd73117 100644
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -49,9 +49,11 @@ public class ConflictTracker extends ListenerAdapter {
   private Node parentNode = new Node(-2);
   private String operation;
   private String detail;
+  private String errorMessage;
   private int depth;
   private int id;
   private boolean manual = false;
+  private boolean conflictFound = false;
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "locationMode";
@@ -132,7 +134,9 @@ public class ConflictTracker extends ListenerAdapter {
       if (confupdates != null && !u.isManual()) {
         for(Update u2: confupdates) {
           if (conflicts(u, u2)) {
-            throw new RuntimeException(createErrorMessage(u, u2));
+            //throw new RuntimeException(createErrorMessage(u, u2));
+            conflictFound = true;
+	    errorMessage = createErrorMessage(u, u2);
           }
         }
       }
@@ -168,9 +172,9 @@ public class ConflictTracker extends ListenerAdapter {
   }
   
   String createErrorMessage(Update u, Update u2) {
-    String message = "Conflict found between the two apps. App"+u.getApp()+
+    String message = "Conflict found between the two apps. "+u.getApp()+
 		     " has written the value: "+u.getValue()+
-      " to the attribute: "+u.getAttribute()+" while App"
+      " to the attribute: "+u.getAttribute()+" while "
       +u2.getApp()+" is writing the value: "
       +u2.getValue()+" to the same variable!";
     System.out.println(message);	
@@ -553,8 +557,13 @@ public class ConflictTracker extends ListenerAdapter {
         ti.setNextPC(nextIns);
       }
     }
-
-    if (conflictSet.contains(LOCATION_VAR)) {
+    
+    if (conflictFound) {
+      StringBuilder sb = new StringBuilder();
+      sb.append(errorMessage);
+      Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+      ti.setNextPC(nextIns);
+    } else if (conflictSet.contains(LOCATION_VAR)) {
       MethodInfo mi = executedInsn.getMethodInfo();
       // Find the last load before return and get the value here
       if (mi.getName().equals(SET_LOCATION_METHOD) &&
@@ -572,19 +581,20 @@ public class ConflictTracker extends ListenerAdapter {
     } else {
       if (executedInsn instanceof WriteInstruction) {
         String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
-        
+         
         for (String var : conflictSet) {
           if (varId.contains(var)) {
             // Get variable info
             byte type = getType(ti, executedInsn);
             String value = getValue(ti, executedInsn, type);
             String writer = getWriter(ti.getStack(), appSet);
+
             // Just return if the writer is not one of the listed apps in the .jpf file
             if (writer == null)
               return;
             
-            if (getWriter(ti.getStack(), manualSet) != null)
-              manual = true;
+            //if (getWriter(ti.getStack(), manualSet) != null)
+            //  manual = true;
             
             // Update the current updates
             writeWriterAndValue(writer, var, value);