// if (state.SSJAVADEBUG) {
// debugPrint();
// }
- // inference();
- parseLocationAnnotation();
- doFlowDownCheck();
- doDefinitelyWrittenCheck();
- doLoopCheck();
+ if (state.SSJAVAINFER) {
+ inference();
+ } else {
+ parseLocationAnnotation();
+ doFlowDownCheck();
+ doDefinitelyWrittenCheck();
+ doLoopCheck();
+ }
}
private void inference() {
//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;
} 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;
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
then
JAVAOPTS="$JAVAOPTS -ssjavadebug"
+elif [[ $1 = '-ssjavainfer' ]]
+then
+JAVAOPTS="$JAVAOPTS -ssjavainfer"
+
elif [[ $1 = '-ssjava-inject-error' ]]
then
USE_SSJAVA_CLASSPATH=true