Menu
▾
▴
javapathfinder-devel — development related topics (your place if you work with the sources)
You can subscribe to this list here.
| 2005 |
Jan
|
Feb
|
Mar
|
Apr
(9) |
May
(38) |
Jun
(13) |
Jul
(3) |
Aug
(14) |
Sep
(25) |
Oct
(44) |
Nov
(6) |
Dec
(2) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2006 |
Jan
(4) |
Feb
(14) |
Mar
(16) |
Apr
(2) |
May
(1) |
Jun
(2) |
Jul
(2) |
Aug
(1) |
Sep
(1) |
Oct
|
Nov
(3) |
Dec
(1) |
| 2007 |
Jan
(3) |
Feb
(39) |
Mar
(30) |
Apr
(31) |
May
(20) |
Jun
(72) |
Jul
(41) |
Aug
(78) |
Sep
(48) |
Oct
(59) |
Nov
(31) |
Dec
(47) |
| 2008 |
Jan
(18) |
Feb
(37) |
Mar
(45) |
Apr
(78) |
May
(16) |
Jun
|
Jul
(8) |
Aug
(10) |
Sep
(23) |
Oct
(10) |
Nov
(12) |
Dec
(1) |
| 2009 |
Jan
(4) |
Feb
|
Mar
(3) |
Apr
(1) |
May
(1) |
Jun
(1) |
Jul
|
Aug
|
Sep
(1) |
Oct
(3) |
Nov
(2) |
Dec
|
| 2010 |
Jan
(1) |
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2013 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(2) |
Oct
|
Nov
|
Dec
|
|
From: Michal K. <mic...@gm...> - 2008-11-15 16:43:06
|
Hi, may vm.classpath and vm.sourcepath contain paths to jar files? Michal |
|
From: Mateusz U. <mat...@gm...> - 2008-11-11 20:54:46
|
Hi,
In my project (implementing java.util.concurrent) I've
encountered a problem. We have one example
that runs ReentrantLock.lock()/unlock() in few concurrent threads, we
use this to test our performance
against code from original SDK. When we want to test code from SDK we
need to change the names
of our classes, for example JPF_java_util_concurrent_locks_ReentrantLock
to JPF_java_util_concurrent_locks_ReentrantLock2.
We could avoid this by setting appropriate vm.peer.packages but the
problem is that our peer classes
are in gov.nasa.jpf.jvm package which is always included. One thing that
we can do is to change the
package from gov.nasa.jpf.jvm but it seems that my code will not be
complaint with JPF coding conventions.
Is there a another solution for that ?
Yours sincerely
Mateusz Ujma - GSoC student
|
|
From: Corina P. <Cor...@na...> - 2008-11-08 00:19:28
|
Taehoon Lee wrote: > Hi, > I found a bug in extension/symbc. > > 1. The extension create the object of the class SymbolicInstructionFactory. > 2. the constructor of the class SymbolicInstructionFactory invoke the > constructor of the class GenericInstructionFactory. > 3. the constructor of the class genericInstructionFactory invoke the > createMaps(). > 4. loader.loadClass() is invoked. loader is defined in the Class > DefaultInstructionFactory. > 5. At this time, The loader is not initiallized. > > > You should use: +vm.insn.factory.class and +vm.peer.packages in the JPF config. I updated the Readme file. Thanks, -- Corina Pasareanu, PhD CMU/NASA Ames http://ti.arc.nasa.gov/profile/pcorina/ |
|
From: Pasareanu, C. S. (ARC-TI)[S. G. T. INC.] <Cor...@na...> - 2008-11-07 08:59:44
|
no -- not yet. Corina Pasareanu, PhD http://ase.arc.nasa.gov/people/pcorina/ -----Original Message----- From: Taehoon Lee [mailto:ta...@ky...] Sent: Fri 11/7/2008 1:11 AM To: jav...@li... Subject: [Javapathfinder-devel] Can JPF generate String based test input ? Hi, I have a question about symbolic execution. I want to generate tests from Java based Calculator. Given String("1+2" or "3*4+5"), Calculator compute the result(3 or 17). example) int calculator(String); Is it possible that JPF generate the String based test input? -- ------------------------------------------------------ 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...@ky... ------------------------------------------------------- ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Javapathfinder-devel mailing list Jav...@li... https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel |
|
From: Pasareanu, C. S. (ARC-TI)[S. G. T. INC.] <Cor...@na...> - 2008-11-07 08:45:44
|
do you have the example on which this happens? thanks. Corina Pasareanu, PhD http://ase.arc.nasa.gov/people/pcorina/ -----Original Message----- From: Taehoon Lee [mailto:ta...@ky...] Sent: Fri 11/7/2008 12:45 AM To: jav...@li... Subject: [Javapathfinder-devel] I found a bug in extension/symbc Hi, I found a bug in extension/symbc. 1. The extension create the object of the class SymbolicInstructionFactory. 2. the constructor of the class SymbolicInstructionFactory invoke the constructor of the class GenericInstructionFactory. 3. the constructor of the class genericInstructionFactory invoke the createMaps(). 4. loader.loadClass() is invoked. loader is defined in the Class DefaultInstructionFactory. 5. At this time, The loader is not initiallized. -- ------------------------------------------------------ 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...@ky... ------------------------------------------------------- ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ Javapathfinder-devel mailing list Jav...@li... https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel |
|
From: Taehoon L. <ta...@ky...> - 2008-11-07 07:11:29
|
Hi,
I have a question about symbolic execution.
I want to generate tests from Java based Calculator.
Given String("1+2" or "3*4+5"), Calculator compute the result(3 or 17).
example) int calculator(String);
Is it possible that JPF generate the String based test input?
--
------------------------------------------------------
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...@ky...
-------------------------------------------------------
|
|
From: Taehoon L. <ta...@ky...> - 2008-11-07 06:45:48
|
Hi, I found a bug in extension/symbc. 1. The extension create the object of the class SymbolicInstructionFactory. 2. the constructor of the class SymbolicInstructionFactory invoke the constructor of the class GenericInstructionFactory. 3. the constructor of the class genericInstructionFactory invoke the createMaps(). 4. loader.loadClass() is invoked. loader is defined in the Class DefaultInstructionFactory. 5. At this time, The loader is not initiallized. -- ------------------------------------------------------ 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...@ky... ------------------------------------------------------- |
|
From: Peter C. M. <Pet...@na...> - 2008-11-04 02:49:48
|
for consistency reasons, rev 1057 changed the "vm.peer_packages" property into "vm.peer.packages". Please update your Eclipse launch configs and *.jpf mode property files accordingly. Sorry for the inconvenience. It's all in the name of extension mechanism specific classpaths for listeners, peers and instructions, which are now supported via jpf.listener.classpath vm.peer.classpath vm.insn_factory.classpath Now you should be able to have your extensions outside of the JPF distrib and/or SuT project. -- Peter |
|
From: Taehoon L. <ta...@ky...> - 2008-10-27 07:27:34
|
Hi, Is there any way to convert ClassInfo to Class? I would like to invoke ResourceManager.getProperty(). "public static native String getProperty(String propName, Hashtable env,Context ctx, boolean concat);" I think that Using MJI is good for get return value of this method. However, I don't know how can I translate JPF class to JVM class. -- ------------------------------------------------------ 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...@ky... ------------------------------------------------------- |
|
From: Taehoon L. <ta...@ky...> - 2008-10-10 18:11:20
|
Hi, I would like to indroduce new extension which verify XPDL via JPF.The XPDL is a business process definition language. The XPDL verification framework is similar to statechart model checking extension. If no one disapprove my contribution, I will commit the code within a week.-- Taehoon Lee |
|
From: Peter C. M. <Pet...@na...> - 2008-10-10 16:35:40
|
the problem would be synchronization bottlenecks. If you have distributed searches and a single state repository for matching/ restoring, this would require an amount of synchronization that would probably slow things down considerably. What could work is to allow some redundancy, i.e. let nodes proceed independently of each other, but IMHO this requires some knowledge about the shape of the state space, to decide which branch points should spawn remote searches. I think partitioning into execution, state management and report generation is more promising in the near to mid future. For example, one of the major memory sinks is simply storing traces (the Transition Steps). I think that could easily be factorized out into a different process/node, not requiring much synchronization -- Peter On Oct 9, 2008, at 8:21 AM, Mateusz Ujma wrote: > Hi, > > Would it be possible to write parallel version of JPF that will use > MPI ? > > Yours sincerely > > Mateusz Ujma > > ------------------------------------------------------------------------- > This SF.Net email is sponsored by the Moblin Your Move Developer's > challenge > Build the coolest Linux based applications with Moblin SDK & win > great prizes > Grand prize is a trip for two to an Open Source event anywhere in > the world > http://moblin-contest.org/redirect.php?banner_id=100&url=/ > _______________________________________________ > Javapathfinder-devel mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel |
|
From: Peter C. M. <Pet...@na...> - 2008-10-10 16:23:02
|
the problem is that JPF runs should be reproducible (on different machines/OSes/times). If you use a random seed, they wouldn't, so this shouldn't be the default. But I agree that we should have an option for random seeds. -- Peter On Oct 10, 2008, at 8:03 AM, Marco Ferreira wrote: > Currently, in ChoiceGenerator.java, the random generator is > initialized with a seed of 42 except if cg.seed is specified. This > means that the choice generator is not "as random" as it could be. > Wouldn't it be a better idea to initialize it with "new Random()" > (using the system time as seed) except if cg.seed is specified (using > the specified value instead in that case)? > > I've attached a .patch file with the required changes to > ChoiceGenerator.java in case you agree with me... > > Best regards, > Marco > < > ChoiceGeneratorNoDefaultSeed > .patch > > > ------------------------------------------------------------------------- > This SF.Net email is sponsored by the Moblin Your Move Developer's > challenge > Build the coolest Linux based applications with Moblin SDK & win > great prizes > Grand prize is a trip for two to an Open Source event anywhere in > the world > http://moblin-contest.org/redirect.php?banner_id=100&url=/_______________________________________________ > Javapathfinder-devel mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel |
|
From: Marco F. <mp...@es...> - 2008-10-10 15:03:15
|
Currently, in ChoiceGenerator.java, the random generator is initialized with a seed of 42 except if cg.seed is specified. This means that the choice generator is not "as random" as it could be. Wouldn't it be a better idea to initialize it with "new Random()" (using the system time as seed) except if cg.seed is specified (using the specified value instead in that case)? I've attached a .patch file with the required changes to ChoiceGenerator.java in case you agree with me... Best regards, Marco |
|
From: Taehoon L. <ta...@ky...> - 2008-10-10 08:08:57
|
I think it is possible, but it is not easy. Mateusz Ujma 쓴 글: > Hi, > > Would it be possible to write parallel version of JPF that will use > MPI ? > > Yours sincerely > > Mateusz Ujma > > ------------------------------------------------------------------------- > This SF.Net email is sponsored by the Moblin Your Move Developer's challenge > Build the coolest Linux based applications with Moblin SDK & win great prizes > Grand prize is a trip for two to an Open Source event anywhere in the world > http://moblin-contest.org/redirect.php?banner_id=100&url=/ > _______________________________________________ > Javapathfinder-devel mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel > > -- ------------------------------------------------------ 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...@ky... ------------------------------------------------------- |
|
From: Mateusz U. <mat...@gm...> - 2008-10-09 15:21:06
|
Hi,
Would it be possible to write parallel version of JPF that will use
MPI ?
Yours sincerely
Mateusz Ujma
|
|
From: Peter C. M. <Pet...@na...> - 2008-10-02 23:09:14
|
lots of - TestVMDeadlock for instance -- Peter On Oct 2, 2008, at 1:25 PM, Michal Kebrt wrote: > Hi, > > are there any test programs violating NotDeadlockedProperty in JPF > sources? > > MK |
|
From: Michal K. <mic...@gm...> - 2008-10-02 20:25:53
|
Hi, are there any test programs violating NotDeadlockedProperty in JPF sources? MK |
|
From: Michal K. <mic...@gm...> - 2008-10-01 21:01:18
|
Hi,
I have this piece of code run under JPF and it seems Thread.sleep doesn't work
correctly. The native sleep method always ends in this branch.
if (!ti.isFirstStepInsn()) { // first time we see this (may be the only time)
// nothing to do, we are good to go
}
@Test
public void sleep() {
try {
Thread.sleep(1000);
} catch (InterruptedException e) {
e.printStackTrace();
}
}
MK
|
|
From: Michal K. <mic...@gm...> - 2008-09-29 15:42:45
|
No it is not at the end of a JPF run. It's in a native peer for JUnit listener,
e.g.:
public static void testStartedNative(MJIEnv env, int robj, int rString0) {
System.out.println(env.getJPF().getReporter().getPath().size());
}
MK
Peter C. Mehlitz wrote:
> If you inspect the path at the end of a JPF run, it is only non-empty
> in case there was a property violation (backtracking to the first
> state and not having any non-processed choice anymore *is* the end
> condition for the search)
>
> -- Peter
>
>
> On Sep 29, 2008, at 6:13 AM, Michal Kebrt wrote:
>
>> After writing a part of JUnitProperty I realized it wouldn't be so
>> straightforward as it seemed to be. For example, JUnit has
>> @Test(expected=...) annotation which shouldn't produce an error when
>> expected exception occurs. Therefore the JUnitProperty should
>> understand some of JUnit internals which is not very clean solution.
>>
>> I am thinking of inspecting JVM Path object (and maybe other
>> information provided by Reporter) in JUnit's native peer but the
>> path is always empty, why?
>>
>> MK
>
>
> -------------------------------------------------------------------------
> This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
> Build the coolest Linux based applications with Moblin SDK & win great prizes
> Grand prize is a trip for two to an Open Source event anywhere in the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
|
|
From: Peter C. M. <Pet...@na...> - 2008-09-29 15:34:20
|
If you inspect the path at the end of a JPF run, it is only non-empty in case there was a property violation (backtracking to the first state and not having any non-processed choice anymore *is* the end condition for the search) -- Peter On Sep 29, 2008, at 6:13 AM, Michal Kebrt wrote: > After writing a part of JUnitProperty I realized it wouldn't be so > straightforward as it seemed to be. For example, JUnit has > @Test(expected=...) annotation which shouldn't produce an error when > expected exception occurs. Therefore the JUnitProperty should > understand some of JUnit internals which is not very clean solution. > > I am thinking of inspecting JVM Path object (and maybe other > information provided by Reporter) in JUnit's native peer but the > path is always empty, why? > > MK |
|
From: Michal K. <mic...@gm...> - 2008-09-29 13:13:47
|
After writing a part of JUnitProperty I realized it wouldn't be so straightforward as it seemed to be. For example, JUnit has @Test(expected=...) annotation which shouldn't produce an error when expected exception occurs. Therefore the JUnitProperty should understand some of JUnit internals which is not very clean solution. I am thinking of inspecting JVM Path object (and maybe other information provided by Reporter) in JUnit's native peer but the path is always empty, why? MK Peter C. Mehlitz wrote: > this is the problem I was thinking of - if you run JUnit under JPF, > the JUnit exception firewall is a perfectly fine exception handler > from JPF's perspective, so NoUnhandledExceptionProperty is never > violated. You can't say JUnit is part of the SuT, but a little less > than the rest. Both vm.halt_on_throw and overriding > JVM.handleException() are hacks in this case. The only clean solution > I see is to create a new PropertyListener, say JUnitProperty, which > monitors exceptionThrown, and turns the ones underneath JUnit into > property violations > > -- Peter |
|
From: Peter C. M. <Pet...@na...> - 2008-09-24 23:34:18
|
this is the problem I was thinking of - if you run JUnit under JPF, the JUnit exception firewall is a perfectly fine exception handler from JPF's perspective, so NoUnhandledExceptionProperty is never violated. You can't say JUnit is part of the SuT, but a little less than the rest. Both vm.halt_on_throw and overriding JVM.handleException() are hacks in this case. The only clean solution I see is to create a new PropertyListener, say JUnitProperty, which monitors exceptionThrown, and turns the ones underneath JUnit into property violations -- Peter On Sep 24, 2008, at 11:31 AM, Michal Kebrt wrote: > Hello, > > I've just tried to run the Racer example under JPF+JUnit. It > correctly prints > '10' twice and then 'java.lang.ArithmeticException: division by > zero'. But this > exception is eaten in JUnit internals so the propertyViolated method > is not > called. Is there a way to get execution history (as shown in > example) in such > situation? Throwing exception out of JUnit would probably help but I > would to > avoid it. I don't want to modify neither JUnit nor JPF, just want to > extend both > of them. > > Michal > > ------------------------------------------------------------------------- > This SF.Net email is sponsored by the Moblin Your Move Developer's > challenge > Build the coolest Linux based applications with Moblin SDK & win > great prizes > Grand prize is a trip for two to an Open Source event anywhere in > the world > http://moblin-contest.org/redirect.php?banner_id=100&url=/ > _______________________________________________ > Javapathfinder-devel mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel |
|
From: Michal K. <mic...@gm...> - 2008-09-24 18:32:14
|
Hello, I've just tried to run the Racer example under JPF+JUnit. It correctly prints '10' twice and then 'java.lang.ArithmeticException: division by zero'. But this exception is eaten in JUnit internals so the propertyViolated method is not called. Is there a way to get execution history (as shown in example) in such situation? Throwing exception out of JUnit would probably help but I would to avoid it. I don't want to modify neither JUnit nor JPF, just want to extend both of them. Michal |
|
From: Peter C. M. <Pet...@na...> - 2008-09-18 11:12:55
|
fixed.
StringWriter and PrintWriter are pure Java, i.e. don't need native peers
The Throwable model class had <2do> stub methods for the
printStackTraces
-- Peter
On Sep 17, 2008, at 9:14 AM, Michal Kebrt wrote:
> Hi,
>
> any news?
>
> Michal
>
> Michal Kebrt wrote:
>> Hi,
>>
>> I have this piece of code (part of JUnit internals) run under JPF:
>>
>> public String getTrace() {
>> StringWriter stringWriter= new StringWriter();
>> PrintWriter writer= new PrintWriter(stringWriter);
>> getException().printStackTrace(writer);
>> StringBuffer buffer= stringWriter.getBuffer();
>> return buffer.toString();
>> }
>>
>> It always returns empty string which a surprise for me because I
>> can't
>> find StringWriter and PrintWriter classes implemented in JPF. Why JPF
>> doesn't throw java.lang.UnsatisfiedLinkError? And is there a chance
>> these classes will be implemented soon?
>>
>> Michal
|
|
From: John P. <jp...@go...> - 2008-09-18 03:15:30
|
excellent. Peter's inbox is our issue tracker (and resolver!) jp On Thu, Sep 18, 2008 at 12:08 PM, Taehoon Lee <no...@gm...> wrote: > It is already solved. > > http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1003&view=rev > > > 2008년 9월 18일 (목) 오후 7:01, John Penix <jp...@go...>님의 말: >> >> Hi Taehoon, >> >> Did you look to see if there is an obvious problem in the code? >> >> Peter - should we track issues on SourceForge? (do we already to this?) >> >> John >> >> 2008/9/3 Taehoon Lee <no...@gm...>: >> > example is atteched. >> > >> > The result of example on JPF is as follows. >> > ------------------------------------- >> > class void >> > null >> > class java.lang.Class >> > class int >> > class boolean >> > class java.lang.String >> > class void >> > class void >> > class void >> > class void >> > class void >> > ------------------------------------ >> > >> > The result of example on JVM is as follows. >> > ------------------------------------- >> > void >> > class java.io.File >> > int >> > class java.lang.Class >> > void >> > void >> > void >> > boolean >> > class java.lang.String >> > void >> > void >> > ----------------------------------- >> > >> > -- >> > -- >> > Taehoon Lee(이태훈) >> > Ph.D candidate >> > Kyonggi University , Korea >> > >> > >> > >> > ------------------------------------------------------------------------- >> > This SF.Net email is sponsored by the Moblin Your Move Developer's >> > challenge >> > Build the coolest Linux based applications with Moblin SDK & win great >> > prizes >> > Grand prize is a trip for two to an Open Source event anywhere in the >> > world >> > http://moblin-contest.org/redirect.php?banner_id=100&url=/ >> > _______________________________________________ >> > Javapathfinder-devel mailing list >> > Jav...@li... >> > https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel >> > >> > > > > > -- > -- > Taehoon Lee(이태훈) > Ph.D candidate > Kyonggi University , Korea > > |
