Re: [Javapathfinder-user] Symbolic execution problem.

[Corina P. <Cor...@na...>]

could you tell us what is the test program?
why is

2147483647

not a good number?

Corina

Taehoon Lee wrote:
> 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??
>
>