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 4dcaad247404c8d7b9032d1cac3db2942580c082..bf1c6f12df1262f7c36be0b67cd2c4538465881a 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 2193d4972eaa61cc7fae18f34c45dcf31c9b91d5..a3f0a8bcd31acc0db3e9371b08adba723fb37526 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 9b34ddc7bba7b7a1f282d06c56c3b62559dff597..2ec01a630eb17ea5cd3a3775a1e171616182a618 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 2468a2c444e0efb48f68b933a15703358c441e08..28d65c4ca8e55cf56456137f286b4e951eda03db 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