Buildfile: /homes/qsp30/Programs/jpf/jpf-symbc/build.xml

-init:

-compile-annotations:

-compile-main:

-compile-peers:

-compile-classes:

-compile-tests:

-compile-examples:

compile:

-jar-jvm:

-jar-jpf:

-jar-annotations:

build:

test:
    [junit] Running gov.nasa.jpf.symbc.TestBooleanSpecial1
    [junit] Tests run: 1, Failures: 1, Errors: 0, Time elapsed: 1.557 sec
    [junit] Output:
    [junit]   running jpf with args: +jvm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory +symbolic.method=gov.nasa.jpf.symbc.TestBooleanSpecial1.testBooleanInvokeSpecial(sym#sym)
    [junit] Running Symbolic PathFinder ...
    [junit] symbolic.dp=choco
    [junit] symbolic.string_dp_timeout_ms=0
    [junit] symbolic.string_dp=none
    [junit] symbolic.choco_time_bound=30000
    [junit] symbolic.min_int=-1000000
    [junit] symbolic.max_int=1000000
    [junit] symbolic.min_double=-8.0
    [junit] symbolic.max_double=7.0
    [junit] JavaPathfinder v7.0 (rev 1107) - (C) RIACS/NASA Ames Research Center
    [junit] 
    [junit] 
    [junit] ====================================================== system under test
    [junit] gov.nasa.jpf.symbc.TestBooleanSpecial1.runTestMethod()
    [junit] 
    [junit] ====================================================== search started: 04/09/13 11:18
    [junit] 
    [junit] ====================================================== error 1
    [junit] gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
    [junit] java.lang.AssertionError: Bad Path condition in TestBooleanSpecial1.testBoolean1 if (x == true):
    [junit] EXPECTED:
    [junit] one of
    [junit] x_1_SYMINT != CONST_0 && y_2_SYMINT == CONST_0
    [junit] or
    [junit] x_1_SYMINT != CONST_0 && y_2_SYMINT != CONST_0
    [junit] ACTUAL:
    [junit] constraint # = 2
    [junit] x_2_SYMINT != CONST_0 && y_3_SYMINT == CONST_0
    [junit] 
    [junit] 	at gov.nasa.jpf.symbc.BooleanTest.testBoolean(BooleanTest.java:16)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.testBooleanInvokeSpecial(TestBooleanSpecial1.java:24)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.mainTest(TestBooleanSpecial1.java:18)
    [junit] 	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:602)
    [junit] 
    [junit] 
    [junit] ====================================================== snapshot #1
    [junit] thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
    [junit]   call stack:
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:604)
    [junit] 
    [junit] 
    [junit] ====================================================== error 2
    [junit] gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
    [junit] java.lang.AssertionError: Bad Path condition in TestBooleanSpecial1.testBoolean1 (x == false):
    [junit] EXPECTED:
    [junit] one of
    [junit] x_1_SYMINT == CONST_0 && y_2_SYMINT == CONST_0
    [junit] or
    [junit] x_1_SYMINT == CONST_0 && y_2_SYMINT != CONST_0
    [junit] ACTUAL:
    [junit] constraint # = 2
    [junit] x_2_SYMINT == CONST_0 && y_3_SYMINT == CONST_0
    [junit] 
    [junit] 	at gov.nasa.jpf.symbc.BooleanTest.testBoolean(BooleanTest.java:22)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.testBooleanInvokeSpecial(TestBooleanSpecial1.java:24)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.mainTest(TestBooleanSpecial1.java:18)
    [junit] 	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:602)
    [junit] 
    [junit] 
    [junit] ====================================================== snapshot #2
    [junit] thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
    [junit]   call stack:
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:604)
    [junit] 
    [junit] 
    [junit] ====================================================== error 3
    [junit] gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
    [junit] java.lang.AssertionError: Bad Path condition in TestBooleanSpecial1.testBoolean1 if (x == true):
    [junit] EXPECTED:
    [junit] one of
    [junit] x_1_SYMINT != CONST_0 && y_2_SYMINT == CONST_0
    [junit] or
    [junit] x_1_SYMINT != CONST_0 && y_2_SYMINT != CONST_0
    [junit] ACTUAL:
    [junit] constraint # = 2
    [junit] x_2_SYMINT != CONST_0 && y_3_SYMINT != CONST_0
    [junit] 
    [junit] 	at gov.nasa.jpf.symbc.BooleanTest.testBoolean(BooleanTest.java:16)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.testBooleanInvokeSpecial(TestBooleanSpecial1.java:24)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.mainTest(TestBooleanSpecial1.java:18)
    [junit] 	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:602)
    [junit] 
    [junit] 
    [junit] ====================================================== snapshot #3
    [junit] thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
    [junit]   call stack:
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:604)
    [junit] 
    [junit] 
    [junit] ====================================================== error 4
    [junit] gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
    [junit] java.lang.AssertionError: Bad Path condition in TestBooleanSpecial1.testBoolean1 (x == false):
    [junit] EXPECTED:
    [junit] one of
    [junit] x_1_SYMINT == CONST_0 && y_2_SYMINT == CONST_0
    [junit] or
    [junit] x_1_SYMINT == CONST_0 && y_2_SYMINT != CONST_0
    [junit] ACTUAL:
    [junit] constraint # = 2
    [junit] x_2_SYMINT == CONST_0 && y_3_SYMINT != CONST_0
    [junit] 
    [junit] 	at gov.nasa.jpf.symbc.BooleanTest.testBoolean(BooleanTest.java:22)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.testBooleanInvokeSpecial(TestBooleanSpecial1.java:24)
    [junit] 	at gov.nasa.jpf.symbc.TestBooleanSpecial1.mainTest(TestBooleanSpecial1.java:18)
    [junit] 	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:602)
    [junit] 
    [junit] 
    [junit] ====================================================== snapshot #4
    [junit] thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,lockCount:0,suspendCount:0}
    [junit]   call stack:
    [junit] 	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:604)
    [junit] 
    [junit] 
    [junit] ====================================================== results
    [junit] error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError: Bad Path condition in Te..."
    [junit] error #2: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError: Bad Path condition in Te..."
    [junit] error #3: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError: Bad Path condition in Te..."
    [junit] error #4: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError: Bad Path condition in Te..."
    [junit] 
    [junit] ====================================================== search finished: 04/09/13 11:18
    [junit] 

BUILD FAILED
/homes/qsp30/Programs/jpf/jpf-symbc/build.xml:235: Test gov.nasa.jpf.symbc.TestBooleanSpecial1 failed

Total time: 3 seconds