[Javapathfinder-user] Symbolic execution problem.

[Taehoon L. <ta...@kg...>]

Hi, My name is Taehoon

I have two question
first, Could you tell me the difference between extension/symbolic and
extension/symbc

secondly

When I execute JPF in Symbolic Execution Mode with following options,
----------------------------------------------------------------------------------
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=. +vm.storage.class= +symbolic.method=myMethod(sym#sym)
+jpf.report.console.finished= MyClass1
----------------------------------------------------------------------------------

I receive following results

----------------------------------------------------------------------------------
Execute symbolic INVOKESPECIAL: myMethod2(II)I ( x_1_SYMINT, y_2_SYMINT )

MyClass2.myMethod2 Path Condition: # = 2
x_1_SYMINT[2147483647] >= CONST_5 && (y_2_SYMINT[2147483647] +
x_1_SYMINT[2147483647]) > CONST_0

MyClass2.myMethod2 Path Condition: # = 2
x_1_SYMINT[2147483647] < CONST_5 && (y_2_SYMINT[2147483647] +
x_1_SYMINT[2147483647]) <= CONST_0
----------------------------------------------------------------------------------

I think the number 2147483647 is not correct test input data.
The JPF which is in subversion repository is unstable??

-- 
------------------------------------------------------
Taehoon Lee

Department of Computer Science
Kyonggi University
San94-6, Yiui-dong, Yongtong-gu, Suwon-si, 442-760, South Korea
TEL: +82-11-9932-2732
FAX: +82-31-249-9673
EMAIL: ta...@ky...
-------------------------------------------------------