From: yeom <yeom>
Date: Fri, 17 Feb 2012 20:12:54 +0000 (+0000)
Subject: add new compilation flag -ssjavainfer for the location inference.
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=25e0a107717c4ddd7b27a5f9a9fc3385888cef91;p=IRC.git

add new compilation flag -ssjavainfer for the location inference.
---

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 4dcaad24..bf1c6f12 100644
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -118,11 +118,14 @@ public class SSJavaAnalysis {
     // if (state.SSJAVADEBUG) {
     // debugPrint();
     // }
-    // inference();
-    parseLocationAnnotation();
-    doFlowDownCheck();
-    doDefinitelyWrittenCheck();
-    doLoopCheck();
+    if (state.SSJAVAINFER) {
+      inference();
+    } else {
+      parseLocationAnnotation();
+      doFlowDownCheck();
+      doDefinitelyWrittenCheck();
+      doLoopCheck();
+    }
   }
 
   private void inference() {
diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java
index 2193d497..a3f0a8bc 100644
--- a/Robust/src/IR/State.java
+++ b/Robust/src/IR/State.java
@@ -148,6 +148,7 @@ public class State {
   //SSJava
   public boolean SSJAVA=false;
   public boolean SSJAVADEBUG=false;
+  public boolean SSJAVAINFER=false;
   public boolean SSJAVA_GENCODE_PREVENT_CRASHES=false;
   public boolean SSJAVA_INJECT_ERROR=false;
   public int     SSJAVA_INV_ERROR_PROB=0;
diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java
index 9b34ddc7..2ec01a63 100644
--- a/Robust/src/Main/Main.java
+++ b/Robust/src/Main/Main.java
@@ -391,7 +391,8 @@ public class Main {
 
       } else if (option.equals("-ssjavadebug")) {
         state.SSJAVADEBUG = true;
-
+      } else if (option.equals("-ssjavainfer")) {
+        state.SSJAVAINFER= true;
       } else if( option.equals( "-ssjava-inject-error" ) ) {
         state.SSJAVA_GENCODE_PREVENT_CRASHES = true;
         state.SSJAVA_INJECT_ERROR   = true;
diff --git a/Robust/src/buildscript b/Robust/src/buildscript
index 2468a2c4..28d65c4c 100755
--- a/Robust/src/buildscript
+++ b/Robust/src/buildscript
@@ -125,6 +125,7 @@ echo
 echo SSJava options
 echo -ssjava enables SSJava
 echo -ssjavadebug reports interim results
+echo -ssjavainfer location type inference
 echo -ssjava-induce-error N S where 1/N is the probability to error at any deref or divide and S is a random seed
 echo
 echo Other options
@@ -682,6 +683,10 @@ elif [[ $1 = '-ssjavadebug' ]]
 then
 JAVAOPTS="$JAVAOPTS -ssjavadebug"
 
+elif [[ $1 = '-ssjavainfer' ]]
+then
+JAVAOPTS="$JAVAOPTS -ssjavainfer"
+
 elif [[ $1 = '-ssjava-inject-error' ]]
 then
 USE_SSJAVA_CLASSPATH=true