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 4dcaad2..bf1c6f1 100644 (file)
--- 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 2193d49..a3f0a8b 100644 (file)
--- 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 9b34ddc..2ec01a6 100644 (file)
--- 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 2468a2c..28d65c4 100755 (executable)
--- 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