javapathfinder-user — usage related topics (installing, running, options, output...)

[Javapathfinder-user] JPF+JUnit

[Michal K. <mic...@gm...>]

Hello,

I'm trying to run my JUnit tests through JPF but I still cannot succeed. The 
test looks like this:

import org.junit.Test;
import static org.junit.Assert.*;

public class Simple {

     public static void main(String[] args) {
         System.out.println("Hello");
         assertEquals( 4, 4 );
     }

     @Test
     public void add() {
         assertEquals( 4, 4 );
     }
}

When I run it using:

./jpf +vm.classpath=/mypath/junit/junit-4.4.jar:/mypath/junit 
org.junit.runner.JUnitCore Simple

the following error occurs:

gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.reflect.InvocationTargetException: in java.lang.Class.getAnnotations : 
java.lang.NullPointerException
         at java.lang.Class.getAnnotations(Native Method)
         at 
org.junit.internal.runners.JUnit4ClassRunner.classAnnotations(JUnit4ClassRunner.java:64)
         at 
org.junit.internal.runners.JUnit4ClassRunner.getDescription(JUnit4ClassRunner.java:56)
         at 
org.junit.internal.runners.CompositeRunner.getDescription(CompositeRunner.java:40)
         at org.junit.runner.JUnitCore.run(JUnitCore.java:129)
         at org.junit.runner.JUnitCore.run(JUnitCore.java:109)
         at org.junit.runner.JUnitCore.run(JUnitCore.java:100)
         at org.junit.runner.JUnitCore.runMain(JUnitCore.java:81)
         at org.junit.runner.JUnitCore.main(JUnitCore.java:44)

When I run the test without JPF, it works fine. When I run JPF with 'Simple' 
program as an input, it also works fine. Is there some way how to run JPF on 
that test without explicitly writing the main method for each test class as you 
do in your JPF Test Tystem?

Is this problem connected with some reflection limitations in JPF as can be 
found here:
http://sourceforge.net/mailarchive/message.php?msg_id=e3a26fee0605222246x6f3f600as1f9d0484047fa3ce%40mail.google.com

Thanks for answer.

Michal Kebrt

Re: [Javapathfinder-user] JPF - increase memory? (statechart extension)

[<wo...@in...>]

Hello Peter,

I tried all your suggestions.
My commands were most of the time:
+log.info=gov.nasa.jpf.sc  gov.nasa.jpf.sc.StateMachine Statechart
+jpf.report.console.property_violation=error:snapshot
+jpf.listener=.tools.ChoiceTracker
+choice.class=.jvm.choice.sc.SCEventGenerator

and sometimes:
+search.depth_limit=8 (to find a trace with 7 steps)

I have boolean and string variables which are checked (in guards) or set
(in actions). In my small example it worked fine with ChoiceTracker and I
found a trace to tripmode:
the variable was false at the beginning: boolean tripmodeactive = false
an action to set tripmode:
void setTripmode(){tripmodeactive = true;}
I have a guard with tripmode-check (and the constraint to check):
assert !tripmodeactive : "Tripmode = true";
if (tripmodeactive) {
  setNextState(stateC507_10235);
} else {
  setNextState(stateC507_179);
}

The following trace was shown:
====================================================== choice trace #1
INPUT_RIGHTtoC179()
INPUT_PRESStoC180()
INPUT_NAVItoC181()
INPUT_WESTtoC182()
INPUT_OPTIONStoC183()
INPUT_PRESStoC184()
INPUT_RIGHTtoC185()

This is what I was looking for. So I started to test the huge model, but
here it always stops like that:

[SEVERE] JPF out of memory

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       0:01:00
states:             new=77, visited=78, backtracked=78, end=0
search:             maxDepth=76, constraints=0
choice generators:  thread=1, data=77
heap:               gc=230, new=16279, free=175
instructions:       4110692
max memory:         63MB
loaded code:        classes=1735, methods=20281

====================================================== search finished:
14.07.08 14:43

The search states didn't change, when I added the vm-command -xmx512m.
When I start JPF in Eclipse without this command, it takes about 1 or 2
minutes - with the command it takes about 20 minutes. The visited states
etc. are the same. When I added the search-limit with 8, less states were
searched.

I have no large arrays or many instructions, it's just a simple
if-construct for a guard and in an action I assign a new value to a
variable. I have no random variables or threads. I don't use the
Verify.getInt()-commands.
When I changed the +search.min_free property to a higher value, less
states were explored.

I couldn't see the search monitor with the big model, with the small
example it worked.

Thank you very much for your fast replies and support!

Best regards, Elisabeth

> Elisabeth,
>
> the default from the bin/jpf script is -Xmx1024m, which might explain
> why there were less states (apart from a rather small search depth
> limit of 8). Remove the search depth limit, increase the heap, but
> first make sure that JPF instruction logging is turned off (use
> "+jpf.report.console.property_violation=error:snapshot", i.e. no
> 'trace' topic). If you ever get to traces, you probably are more
> interested in UML events than Java instructions, i.e. use the
> ChoiceTracker listener to create event traces.
>
> 6000 transitions should not impose problems, unless your transitions
> contain lots of changes in large arrays and lots of instructions. You
> have to distinguish between UML states and program states, and the
> first step is to find out of they correspond. Are there any threads
> used in our model? Are there random variables? Do you use
> Verify.getInt()/Boolean() etc.? If so, you will have (potentially a
> lot) more program states than UML states.
>
> How does JPF react to the out-of-memory - does it just die, or does it
> report hitting a search constraint? What if you increase the
> +search.min_free property? You can also run with
> +jpf.listener=.tools.SearchMonitor to see how many program states /
> instructions you get executed
>
> -- Peter
>
>
> On Jul 11, 2008, at 8:19 AM, wo...@in... wrote:
>
>> Hello JPF-Team,
>>
>> the JPF Statechart Extension is working well with a small example, but
>> with my huge statechart-model I'll get the message
>>
>>  [SEVERE] JPF out of memory
>>
>> . How can I increase the max memory? Do you have other ideas, how it
>> will
>> work better?
>>
>> I tried the VM-command -Xmx512M and "+search.depth_limit=8" but, as a
>> result, the same or less states were checked. The model is really huge
>> with about 1000 states and 6000 transitions.
>>
>> Thank you very much in advance,
>>
>> Elisabeth
>

Re: [Javapathfinder-user] JPF - increase memory? (statechart extension)

[<wo...@in...>]

It is finite state (or at least should be). There are just boolean and
string variables (altogether about 1400). The integer variables are not
implemented yet.

Maybe it is really just too big. I'm wondering if a model checker like
SPIN or NuSMV could handle the model.

Thank you for your help so far!

Best regards, Elisabeth

> The model may simply be too big.
> Is it finite state? ( am not asking about the number of states in the
> UML statechart, but rather the states that are explored by JPF:  Do you
> have some variables that maybe are incremented in an infinite loop?
> I hope this helps,
> Corina
>
> wo...@in... wrote:
>> Hello JPF-Team,
>>
>> the JPF Statechart Extension is working well with a small example, but
>> with my huge statechart-model I'll get the message
>>
>>   [SEVERE] JPF out of memory
>>
>> . How can I increase the max memory? Do you have other ideas, how it
>> will
>> work better?
>>
>> I tried the VM-command -Xmx512M and "+search.depth_limit=8" but, as a
>> result, the same or less states were checked. The model is really huge
>> with about 1000 states and 6000 transitions.
>>
>> Thank you very much in advance,
>>
>> Elisabeth
>>
>>
>> -------------------------------------------------------------------------
>> Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
>> Studies have shown that voting for your favorite open source project,
>> along with a healthy diet, reduces your potential for chronic lameness
>> and boredom. Vote Now at http://www.sourceforge.net/community/cca08
>> _______________________________________________
>> Javapathfinder-user mailing list
>> Jav...@li...
>> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>>
>
>

Re: [Javapathfinder-user] JPF - increase memory? (statechart extension)

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

The model may simply be too big.
Is it finite state? ( am not asking about the number of states in the 
UML statechart, but rather the states that are explored by JPF:  Do you 
have some variables that maybe are incremented in an infinite loop?
I hope this helps,
Corina

wo...@in... wrote:
> Hello JPF-Team,
>
> the JPF Statechart Extension is working well with a small example, but
> with my huge statechart-model I'll get the message
>
>   [SEVERE] JPF out of memory
>
> . How can I increase the max memory? Do you have other ideas, how it will
> work better?
>
> I tried the VM-command -Xmx512M and "+search.depth_limit=8" but, as a
> result, the same or less states were checked. The model is really huge
> with about 1000 states and 6000 transitions.
>
> Thank you very much in advance,
>
> Elisabeth
>
>
> -------------------------------------------------------------------------
> Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
> Studies have shown that voting for your favorite open source project,
> along with a healthy diet, reduces your potential for chronic lameness
> and boredom. Vote Now at http://www.sourceforge.net/community/cca08
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>   

Re: [Javapathfinder-user] JPF - increase memory? (statechart extension)

[Peter C. M. <Pet...@na...>]

Elisabeth,

the default from the bin/jpf script is -Xmx1024m, which might explain  
why there were less states (apart from a rather small search depth  
limit of 8). Remove the search depth limit, increase the heap, but  
first make sure that JPF instruction logging is turned off (use  
"+jpf.report.console.property_violation=error:snapshot", i.e. no  
'trace' topic). If you ever get to traces, you probably are more  
interested in UML events than Java instructions, i.e. use the  
ChoiceTracker listener to create event traces.

6000 transitions should not impose problems, unless your transitions  
contain lots of changes in large arrays and lots of instructions. You  
have to distinguish between UML states and program states, and the  
first step is to find out of they correspond. Are there any threads  
used in our model? Are there random variables? Do you use  
Verify.getInt()/Boolean() etc.? If so, you will have (potentially a  
lot) more program states than UML states.

How does JPF react to the out-of-memory - does it just die, or does it  
report hitting a search constraint? What if you increase the  
+search.min_free property? You can also run with  
+jpf.listener=.tools.SearchMonitor to see how many program states /  
instructions you get executed

-- Peter


On Jul 11, 2008, at 8:19 AM, wo...@in... wrote:

> Hello JPF-Team,
>
> the JPF Statechart Extension is working well with a small example, but
> with my huge statechart-model I'll get the message
>
>  [SEVERE] JPF out of memory
>
> . How can I increase the max memory? Do you have other ideas, how it  
> will
> work better?
>
> I tried the VM-command -Xmx512M and "+search.depth_limit=8" but, as a
> result, the same or less states were checked. The model is really huge
> with about 1000 states and 6000 transitions.
>
> Thank you very much in advance,
>
> Elisabeth

[Javapathfinder-user] JPF - increase memory? (statechart extension)

[<wo...@in...>]

Hello JPF-Team,

the JPF Statechart Extension is working well with a small example, but
with my huge statechart-model I'll get the message

  [SEVERE] JPF out of memory

. How can I increase the max memory? Do you have other ideas, how it will
work better?

I tried the VM-command -Xmx512M and "+search.depth_limit=8" but, as a
result, the same or less states were checked. The model is really huge
with about 1000 states and 6000 transitions.

Thank you very much in advance,

Elisabeth

Re: [Javapathfinder-user] Problem with newer versions of JPF???

[Marco F. <mp...@es...>]

Thanks for the reply (and the insight about vm.por).

I've been checking the old versions and it stopped working after SVN update
848, Elena's ThreadInfo.createThreadInfo() fix. Restoring ThreadInfo.java to
version 738 (the one before 848 update) makes it work again. So it may be
something related to that fix.

Marco Ferreira

On Tue, Jun 24, 2008 at 12:00 AM, Peter C. Mehlitz <Pet...@na...>
wrote:

> must be a bug in HeuristicSearch, I'll have a look. It works well with
> DFSearch.
>
> BTW - don't use vm.por=false. This is going to be dropped, and can be
> considered non-functional at this point
>
> -- Peter
>
>
>
> On Jun 23, 2008, at 2:51 PM, Marco Ferreira wrote:
>
> > Hi,
> >
> > I'm facing a problem with the latest versions of JPF. I tried to use
> > BFS to search for the deadlock in the DiningPhilosophers problem
> > with only 2 philosophers (so it should be rather quick to find the
> > deadlock). However, after some steps, JPF seems to loop in an
> > infinite cycle in the executeStep() method. Any ideas about what's
> > going on? I've executed JPF on Windows with Java 1.6 using the
> > following command line:
> >
> > java -cp .\build\jpf;.\lib\bcel.jar;.\build\env\jvm;.\build\examples
> > -Xmx512M -Xms512M gov.nasa.jpf.JPF +vm.por=false
> > +search.class=gov.nasa.jpf.search.heuristic.HeuristicSearch
> > +search.heuristic.class=gov.nasa.jpf.search.heuristic.BFSHeuristic
> > DiningPhilosophers.DiningPhilosophers
> >
> > This worked quite well in older versions...
> >
> > Marco Ferreira
>
> -------------------------------------------------------------------------
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services for
> just about anything Open Source.
> http://sourceforge.net/services/buy/index.php
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>

Re: [Javapathfinder-user] Problem with newer versions of JPF???

[Peter C. M. <Pet...@na...>]

must be a bug in HeuristicSearch, I'll have a look. It works well with  
DFSearch.

BTW - don't use vm.por=false. This is going to be dropped, and can be  
considered non-functional at this point

-- Peter



On Jun 23, 2008, at 2:51 PM, Marco Ferreira wrote:

> Hi,
>
> I'm facing a problem with the latest versions of JPF. I tried to use  
> BFS to search for the deadlock in the DiningPhilosophers problem  
> with only 2 philosophers (so it should be rather quick to find the  
> deadlock). However, after some steps, JPF seems to loop in an  
> infinite cycle in the executeStep() method. Any ideas about what's  
> going on? I've executed JPF on Windows with Java 1.6 using the  
> following command line:
>
> java -cp .\build\jpf;.\lib\bcel.jar;.\build\env\jvm;.\build\examples  
> -Xmx512M -Xms512M gov.nasa.jpf.JPF +vm.por=false  
> +search.class=gov.nasa.jpf.search.heuristic.HeuristicSearch  
> +search.heuristic.class=gov.nasa.jpf.search.heuristic.BFSHeuristic  
> DiningPhilosophers.DiningPhilosophers
>
> This worked quite well in older versions...
>
> Marco Ferreira

[Javapathfinder-user] Problem with newer versions of JPF???

[Marco F. <mp...@es...>]

Hi,

I'm facing a problem with the latest versions of JPF. I tried to use BFS to
search for the deadlock in the DiningPhilosophers problem with only 2
philosophers (so it should be rather quick to find the deadlock). However,
after some steps, JPF seems to loop in an infinite cycle in the
executeStep() method. Any ideas about what's going on? I've executed JPF on
Windows with Java 1.6 using the following command line:

java -cp .\build\jpf;.\lib\bcel.jar;.\build\env\jvm;.\build\examples
-Xmx512M -Xms512M gov.nasa.jpf.JPF +vm.por=false
+search.class=gov.nasa.jpf.search.heuristic.HeuristicSearch
+search.heuristic.class=gov.nasa.jpf.search.heuristic.BFSHeuristic
DiningPhilosophers.DiningPhilosophers

This worked quite well in older versions...

Marco Ferreira

Re: [Javapathfinder-user] Question about the statechart extension

[Pasareanu, Corina S. (ARC-TI)[Q. G. INC] <cor...@na...>]

Hello:
In principle, you can use the UML extension (the latest version should be fine).
You will probably need to do some modeling (e.g. for the history vars) -- Peter could comment on that.
I'm working on the topic of generating test sequences for statecharts, so in principle I could help you with that.
Bye,

Corina Pasareanu, PhD
http://ase.arc.nasa.gov/people/pcorina/



-----Original Message-----
From: jav...@li... on behalf of Elisabeth Wolf
Sent: Tue 6/17/2008 2:25 PM
To: jav...@li...
Subject: [Javapathfinder-user] Question about the statechart extension
 
Hello,

I'm a computer science student and working on my diploma thesis about "model-based test case generation". I have a UML statechart diagram with lots of constraints and my task is to derive test cases (input sequences + postconditions) to reach a given state.

Is it possible to use Java Path Finder statechart extension for my problem? Which version works of Java Path Finder would you recommend to me? 

My statechart consists of simple and composed states, initial states, flat history states, and transitions with events, guards and actions. The variables can be boolean, integer and string variables. The statechart is huge, so another question would be: How big could the statechart be to provide feasible results?

Thank you very much in advance!

Best regards & greetings from Germany, Elisabeth Wolf

Re: [Javapathfinder-user] Question about the statechart extension

[Peter C. M. <Pet...@na...>]

Hi Elisabeth,

the UML statechart extension supports all that, except history states. 
You can work off the trunk, there are no changes in the v5 branch reg. 
statecharts. I would not expect scalability problems, since the state 
space of statecharts is usually much smaller than what we experience 
with concurrent programs. Other than the history state, there is only 
one known problem that has to do with premature state matching for 
guided model checking (running with scripts)

-- Peter


Elisabeth Wolf wrote:
> Hello,
>  
> I'm a computer science student and working on my diploma thesis about 
> "model-based test case generation". I have a UML statechart diagram 
> with lots of constraints and my task is to derive test cases (input 
> sequences + postconditions) to reach a given state.
>  
> Is it possible to use Java Path Finder statechart extension for my 
> problem? Which version works of Java Path Finder would you recommend 
> to me?
>  
> My statechart consists of simple and composed states, initial states, 
> flat history states, and transitions with events, guards and actions. 
> The variables can be boolean, integer and string variables. The 
> statechart is huge, so another question would be: How big could the 
> statechart be to provide feasible results?
>  
> Thank you very much in advance!
>  
> Best regards & greetings from Germany, Elisabeth Wolf
>  
> ------------------------------------------------------------------------
>
> -------------------------------------------------------------------------
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services for
> just about anything Open Source.
> http://sourceforge.net/services/buy/index.php
> ------------------------------------------------------------------------
>
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>   

[Javapathfinder-user] Question about the statechart extension

[Elisabeth W. <wo...@in...>]

Hello,

I'm a computer science student and working on my diploma thesis about "model-based test case generation". I have a UML statechart diagram with lots of constraints and my task is to derive test cases (input sequences + postconditions) to reach a given state.

Is it possible to use Java Path Finder statechart extension for my problem? Which version works of Java Path Finder would you recommend to me? 

My statechart consists of simple and composed states, initial states, flat history states, and transitions with events, guards and actions. The variables can be boolean, integer and string variables. The statechart is huge, so another question would be: How big could the statechart be to provide feasible results?

Thank you very much in advance!

Best regards & greetings from Germany, Elisabeth Wolf

Re: [Javapathfinder-user] Volatile variables & Double Checked Locking

[Peter C. M. <Pet...@na...>]

> Java PathFinder can do any kind of check over volatile variables?

JPF doesn't specifically handle volatile - all fields are treated as  
potentially shared, and there is no compilation (JPF is a strict  
interpreter), hence no added caching. The only effect you will see in  
your program is that javac (or whatever bytecode compiler you use)  
will reload the field instead of keeping it on the operand stack or  
locals. There is no difference between one- or two-slot values (long/ 
double), since we treat all writes atomically. If there is a  
potential race, the RaceDetectors will get it anyways.

>   Is there a way to check a Double Checked locking pattern without  
> excluding the fields from lock protection?

not yet. I could see several ways to do that, all based on

(1) the preserved volatile modifier of the field

(2) the associated bytecode pattern, which looks like

   getfield
   if..
   monitorenter
   ..
   getfield
   if..
   ..
   putfield
   monitorexit

This could be done by either providing your own  
+vm.por.fieldlockinfo.class, or - probably more simple - by using a  
BytecodeFactory that overrides the GETFIELD/PUTFIELD insns.

I can't look into this right now, but if you want to work on it I  
would be interested in the result.

-- Peter

[Javapathfinder-user] Volatile variables & Double Checked Locking

[Cristobal J. C. <kry...@ho...>]

Hi,
i have two questions:

Java PathFinder can do any kind of check over volatile variables?
 

Is there a way to check a Double Checked locking pattern without excluding the fields from lock protection?
Thanks in advance,
 
Cristobal J.C.
_________________________________________________________________
Tecnología, moda, motor, viajes,…suscríbete a nuestros boletines para estar siempre a la última
Guapos y guapas, clips musicales y estrenos de cine. 

Re: [Javapathfinder-user] Symbolic execution problem.

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

OK -- I added the solver in the new code.
The mixed integer/real constraints still need to be tested.

Corina

Taehoon Lee wrote:
>
> Thank you for your replies.
>
> However, what I want to know is following test input is correct
>
> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0
>
> and I think difference between versions is not caused by MinMax.java
> Same test input is generated when MinMax.java is reverted to previous 
> version.
>
>
>
> Corina Pasareanu ? ?:
>> The difference between versions comes from the fact that I changed 
>> manually the min/max values in MinMax.java.
>>
>> Corina
>>
>> Taehoon Lee wrote:
>>  
>>> Test program is following
>>>
>>> ------------------------------------------------------------------------------------------------------------ 
>>>
>>> import gov.nasa.jpf.symbc.Debug;
>>>
>>>
>>> public class MyClass1 {
>>> // The method you need tests for
>>> public int myMethod(int x, int y) {
>>> int z = x + y;
>>> if (z > 0) {
>>> z = 1;
>>> } else {
>>> z = z - x;
>>> }
>>> z = x * z;
>>> return z;
>>> }
>>>
>>> // The test driver
>>> public static void main(String[] args) {
>>> MyClass1 mc = new MyClass1();
>>> int x = mc.myMethod(1, 2);
>>> Debug.printPC("\nMyClass1.myMethod Path Condition: ");
>>> }
>>> }
>>> ------------------------------------------------------------------------------------------------------------- 
>>>
>>>
>>> I execute it 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 have two kind of the problem,
>>> first problem is the number of 2147483647 which is the maxinum 
>>> number of int in general case
>>> however JPF generate some condition which is greater than 2147483647.
>>>
>>> second problem, test input is different when version is changed
>>>
>>> with revision 794 in svn, I got following test input
>>>
>>> ====================================================== search 
>>> started: 08. 4. 4 ?? 7:28
>>>
>>> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, 
>>> y_2_SYMINT )
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[-9999] + x_1_SYMINT[10000]) > CONST_0
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[-10000] + x_1_SYMINT[-10000]) <= CONST_0
>>>
>>> ====================================================== search 
>>> finished: 08. 4. 4 ?? 7:28
>>>
>>> with revision 795 in svn, I got following test input
>>> ====================================================== search 
>>> started: 08. 4. 4 ?? 7:31
>>>
>>> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, 
>>> y_2_SYMINT )
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) > CONST_0
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0
>>>
>>> ====================================================== search 
>>> finished: 08. 4. 4 ?? 7:31
>>>
>>>
>>>
>>>
>>> Corina Pasareanu ? ?:
>>>    
>>>> 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??
>>>>>
>>>>>         
>>>>       
>>>     
>>
>>
>> ------------------------------------------------------------------------- 
>>
>> Check out the new SourceForge.net Marketplace.
>> It's the best place to buy or sell services for
>> just about anything Open Source.
>> http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace 
>>
>> _______________________________________________
>> Javapathfinder-user mailing list
>> Jav...@li...
>> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>>
>>   
>
>

Re: [Javapathfinder-user] Symbolic execution problem.

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

I am re-factoring a bit the code to accommodate multiple decision 
procedures.
The solver is not implemented yet.
I'll try to fix it today.
Corina

Taehoon Lee wrote:
>
> Thank you for your replies.
>
> However, what I want to know is following test input is correct
>
> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0
>
> and I think difference between versions is not caused by MinMax.java
> Same test input is generated when MinMax.java is reverted to previous 
> version.
>
>
>
> Corina Pasareanu ? ?:
>> The difference between versions comes from the fact that I changed 
>> manually the min/max values in MinMax.java.
>>
>> Corina
>>
>> Taehoon Lee wrote:
>>  
>>> Test program is following
>>>
>>> ------------------------------------------------------------------------------------------------------------ 
>>>
>>> import gov.nasa.jpf.symbc.Debug;
>>>
>>>
>>> public class MyClass1 {
>>> // The method you need tests for
>>> public int myMethod(int x, int y) {
>>> int z = x + y;
>>> if (z > 0) {
>>> z = 1;
>>> } else {
>>> z = z - x;
>>> }
>>> z = x * z;
>>> return z;
>>> }
>>>
>>> // The test driver
>>> public static void main(String[] args) {
>>> MyClass1 mc = new MyClass1();
>>> int x = mc.myMethod(1, 2);
>>> Debug.printPC("\nMyClass1.myMethod Path Condition: ");
>>> }
>>> }
>>> ------------------------------------------------------------------------------------------------------------- 
>>>
>>>
>>> I execute it 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 have two kind of the problem,
>>> first problem is the number of 2147483647 which is the maxinum 
>>> number of int in general case
>>> however JPF generate some condition which is greater than 2147483647.
>>>
>>> second problem, test input is different when version is changed
>>>
>>> with revision 794 in svn, I got following test input
>>>
>>> ====================================================== search 
>>> started: 08. 4. 4 ?? 7:28
>>>
>>> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, 
>>> y_2_SYMINT )
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[-9999] + x_1_SYMINT[10000]) > CONST_0
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[-10000] + x_1_SYMINT[-10000]) <= CONST_0
>>>
>>> ====================================================== search 
>>> finished: 08. 4. 4 ?? 7:28
>>>
>>> with revision 795 in svn, I got following test input
>>> ====================================================== search 
>>> started: 08. 4. 4 ?? 7:31
>>>
>>> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, 
>>> y_2_SYMINT )
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) > CONST_0
>>>
>>> MyClass1.myMethod Path Condition: # = 1
>>> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0
>>>
>>> ====================================================== search 
>>> finished: 08. 4. 4 ?? 7:31
>>>
>>>
>>>
>>>
>>> Corina Pasareanu ? ?:
>>>    
>>>> 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??
>>>>>
>>>>>         
>>>>       
>>>     
>>
>>
>> ------------------------------------------------------------------------- 
>>
>> Check out the new SourceForge.net Marketplace.
>> It's the best place to buy or sell services for
>> just about anything Open Source.
>> http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace 
>>
>> _______________________________________________
>> Javapathfinder-user mailing list
>> Jav...@li...
>> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>>
>>   
>
>

Re: [Javapathfinder-user] Symbolic execution problem.

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

Thank you for your replies.

However, what I want to know is following test input is correct

(y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0

and I think difference between versions is not caused by MinMax.java
Same test input is generated when MinMax.java is reverted to previous 
version.



Corina Pasareanu ? ?:
> The difference between versions comes from the fact that I changed 
> manually the min/max values in MinMax.java.
>
> Corina
>
> Taehoon Lee wrote:
>   
>> Test program is following
>>
>> ------------------------------------------------------------------------------------------------------------ 
>>
>> import gov.nasa.jpf.symbc.Debug;
>>
>>
>> public class MyClass1 {
>> // The method you need tests for
>> public int myMethod(int x, int y) {
>> int z = x + y;
>> if (z > 0) {
>> z = 1;
>> } else {
>> z = z - x;
>> }
>> z = x * z;
>> return z;
>> }
>>
>> // The test driver
>> public static void main(String[] args) {
>> MyClass1 mc = new MyClass1();
>> int x = mc.myMethod(1, 2);
>> Debug.printPC("\nMyClass1.myMethod Path Condition: ");
>> }
>> }
>> ------------------------------------------------------------------------------------------------------------- 
>>
>>
>> I execute it 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 have two kind of the problem,
>> first problem is the number of 2147483647 which is the maxinum number 
>> of int in general case
>> however JPF generate some condition which is greater than 2147483647.
>>
>> second problem, test input is different when version is changed
>>
>> with revision 794 in svn, I got following test input
>>
>> ====================================================== search started: 
>> 08. 4. 4 ?? 7:28
>>
>> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )
>>
>> MyClass1.myMethod Path Condition: # = 1
>> (y_2_SYMINT[-9999] + x_1_SYMINT[10000]) > CONST_0
>>
>> MyClass1.myMethod Path Condition: # = 1
>> (y_2_SYMINT[-10000] + x_1_SYMINT[-10000]) <= CONST_0
>>
>> ====================================================== search 
>> finished: 08. 4. 4 ?? 7:28
>>
>> with revision 795 in svn, I got following test input
>> ====================================================== search started: 
>> 08. 4. 4 ?? 7:31
>>
>> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )
>>
>> MyClass1.myMethod Path Condition: # = 1
>> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) > CONST_0
>>
>> MyClass1.myMethod Path Condition: # = 1
>> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0
>>
>> ====================================================== search 
>> finished: 08. 4. 4 ?? 7:31
>>
>>
>>
>>
>> Corina Pasareanu ? ?:
>>     
>>> 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??
>>>>
>>>>         
>>>       
>>     
>
>
> -------------------------------------------------------------------------
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services for
> just about anything Open Source.
> http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user
>
>   


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

Ph.D candidate
Department of Computer Science
Kyonggi University
San94-6, Yiui-dong, Yongtong-gu, Suwon-si, 442-760, South Korea
TEL: +82-11-9932-2732
EMAIL: ta...@kg...
-------------------------------------------------------

Re: [Javapathfinder-user] Symbolic execution problem.

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

The difference between versions comes from the fact that I changed 
manually the min/max values in MinMax.java.

Corina

Taehoon Lee wrote:
>
> Test program is following
>
> ------------------------------------------------------------------------------------------------------------ 
>
> import gov.nasa.jpf.symbc.Debug;
>
>
> public class MyClass1 {
> // The method you need tests for
> public int myMethod(int x, int y) {
> int z = x + y;
> if (z > 0) {
> z = 1;
> } else {
> z = z - x;
> }
> z = x * z;
> return z;
> }
>
> // The test driver
> public static void main(String[] args) {
> MyClass1 mc = new MyClass1();
> int x = mc.myMethod(1, 2);
> Debug.printPC("\nMyClass1.myMethod Path Condition: ");
> }
> }
> ------------------------------------------------------------------------------------------------------------- 
>
>
> I execute it 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 have two kind of the problem,
> first problem is the number of 2147483647 which is the maxinum number 
> of int in general case
> however JPF generate some condition which is greater than 2147483647.
>
> second problem, test input is different when version is changed
>
> with revision 794 in svn, I got following test input
>
> ====================================================== search started: 
> 08. 4. 4 ?? 7:28
>
> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )
>
> MyClass1.myMethod Path Condition: # = 1
> (y_2_SYMINT[-9999] + x_1_SYMINT[10000]) > CONST_0
>
> MyClass1.myMethod Path Condition: # = 1
> (y_2_SYMINT[-10000] + x_1_SYMINT[-10000]) <= CONST_0
>
> ====================================================== search 
> finished: 08. 4. 4 ?? 7:28
>
> with revision 795 in svn, I got following test input
> ====================================================== search started: 
> 08. 4. 4 ?? 7:31
>
> Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )
>
> MyClass1.myMethod Path Condition: # = 1
> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) > CONST_0
>
> MyClass1.myMethod Path Condition: # = 1
> (y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0
>
> ====================================================== search 
> finished: 08. 4. 4 ?? 7:31
>
>
>
>
> Corina Pasareanu ? ?:
>>
>> 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??
>>>
>>
>>
>
>

Re: [Javapathfinder-user] Symbolic execution problem.

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

Test program is following

------------------------------------------------------------------------------------------------------------ 

import gov.nasa.jpf.symbc.Debug;


public class MyClass1 {
// The method you need tests for
public int myMethod(int x, int y) {
int z = x + y;
if (z > 0) {
z = 1;
} else {
z = z - x;
}
z = x * z;
return z;
}

// The test driver
public static void main(String[] args) {
MyClass1 mc = new MyClass1();
int x = mc.myMethod(1, 2);
Debug.printPC("\nMyClass1.myMethod Path Condition: ");
}
}
------------------------------------------------------------------------------------------------------------- 


I execute it 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 have two kind of the problem,
first problem is the number of 2147483647 which is the maxinum number of 
int in general case
however JPF generate some condition which is greater than 2147483647.

second problem, test input is different when version is changed

with revision 794 in svn, I got following test input

====================================================== search started: 
08. 4. 4 ?? 7:28

Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[-9999] + x_1_SYMINT[10000]) > CONST_0

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[-10000] + x_1_SYMINT[-10000]) <= CONST_0

====================================================== search finished: 
08. 4. 4 ?? 7:28

with revision 795 in svn, I got following test input
====================================================== search started: 
08. 4. 4 ?? 7:31

Execute symbolic INVOKEVIRTUAL: myMethod(II)I ( x_1_SYMINT, y_2_SYMINT )

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) > CONST_0

MyClass1.myMethod Path Condition: # = 1
(y_2_SYMINT[2147483647] + x_1_SYMINT[2147483647]) <= CONST_0

====================================================== search finished: 
08. 4. 4 ?? 7:31




Corina Pasareanu ? ?:
>
> 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??
>>
>
>


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

Ph.D candidate
Department of Computer Science
Kyonggi University
San94-6, Yiui-dong, Yongtong-gu, Suwon-si, 442-760, South Korea
TEL: +82-11-9932-2732
EMAIL: ta...@kg...
-------------------------------------------------------

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??
>
>   

[Javapathfinder-user] question about symbc

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

Hi,

I think that only one decision procedure is used in symbc,
Do you have any plan to support another decision procedure such as
yices, cvc

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

Ph.D candidate
Department of Computer Science
Kyonggi University
San94-6, Yiui-dong, Yongtong-gu, Suwon-si, 442-760, South Korea
TEL: +82-11-9932-2732
EMAIL: ta...@kg...
-------------------------------------------------------

[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...
-------------------------------------------------------

Re: [Javapathfinder-user] New to PathFinder

[Peter C. M. <Pet...@na...>]

java.lang.ClassLoader is modeled (in env/..), and the model doesn't  
have a getSystemResource() method yet (getResource() is implemented).

-- Peter


On Mar 28, 2008, at 6:59 AM, Jorge Merlino wrote:
> Hi all,
>
> I'm trying to use pathfinder to debug some synchronization issues I  
> have with
> a java program. My problem is that I get this exception in the  
> third line of
> the program:
>
> gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
> java.lang.NoSuchMethodException:
> java.lang.ClassLoader.getSystemResource(Ljava/lang/String;)Ljava/ 
> net/URL;
>     at org.apache.log4j.helpers.Loader.getResource(Loader.java:124)
>     at org.apache.log4j.LogManager.<clinit>(LogManager.java:103)
>     at org.apache.log4j.Logger.getLogger(Logger.java:117)
>     at uy.com.teledata.jastserv.JastServ.main(JastServ.java:31)
>
> which is this:
>
> final Logger logger = Logger.getLogger(JastServ.class);
>
> As you see it is calling log4j and the exception appears inside  
> log4j code.
> Obviously I don't have such exception when running the program with  
> the sun
> jvm and the same classpath.
>
> Can anyone help me with this problem?
>
> Best regards
> 	Jorge
>
> ---------------------------------------------------------------------- 
> ---
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services for
> just about anything Open Source.
> http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/ 
> marketplace
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user

[Javapathfinder-user] New to PathFinder

[Jorge M. <jor...@ip...>]

Hi all,

I'm trying to use pathfinder to debug some synchronization issues I have with 
a java program. My problem is that I get this exception in the third line of 
the program:

gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: 
java.lang.ClassLoader.getSystemResource(Ljava/lang/String;)Ljava/net/URL;
    at org.apache.log4j.helpers.Loader.getResource(Loader.java:124)
    at org.apache.log4j.LogManager.<clinit>(LogManager.java:103)
    at org.apache.log4j.Logger.getLogger(Logger.java:117)
    at uy.com.teledata.jastserv.JastServ.main(JastServ.java:31)

which is this:

final Logger logger = Logger.getLogger(JastServ.class);

As you see it is calling log4j and the exception appears inside log4j code. 
Obviously I don't have such exception when running the program with the sun 
jvm and the same classpath.

Can anyone help me with this problem?

Best regards
	Jorge

[Javapathfinder-user] subscription request

[Krishna K. B <bk...@tc...>]

-- 
regards,
Krishna Kumar B
MECSE132 (06CS11)
TCE
Madurai


-----------------------------------------
This email was sent using TCEMail Service.
Thiagarajar College of Engineering
Madurai - 625015 (India)