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: Corina P. <cor...@na...> - 2013-09-03 20:15:44
|
hi they should be compatible. we just submitted a new version and there were a few glitches corina On 09/03/2013 01:10 PM, Anwesha Das wrote: > Hi, > > I am using the jpf-core along with jpf-symbc. I need to modify the > source code of jpf-symbc. I am unable to compile jpf-symbc because of > missing packages certain import statements do not work. I have used the > mercurial links available for download for both jpf-core and jpf-symbc( > http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc). Can anyone > please help me fix the issue of jpf-symbc compilation? If jpf-core and > jpf-symbc are incompatible, how do I know the compatible version of > jpf-core for the available jpf-symbc? > > Any immediate help would be really helpful. > > Thanks and Regards, > Anwesha > ------------------------------------------------------------------------------ > Learn the latest--Visual Studio 2012, SharePoint 2013, SQL 2012, more! > Discover the easy way to master current and previous Microsoft technologies > and advance your career. Get an incredible 1,500+ hours of step-by-step > tutorial videos with LearnDevNow. Subscribe today and save! > http://pubads.g.doubleclick.net/gampad/clk?id=58040911&iu=/4140/ostg.clktrk > _______________________________________________ > Javapathfinder-devel mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel -- Corina Pasareanu CMU SV, NASA Ames http://ti.arc.nasa.gov/profile/pcorina |
|
From: Anwesha D. <ad...@nc...> - 2013-09-03 20:10:45
|
Hi, I am using the jpf-core along with jpf-symbc. I need to modify the source code of jpf-symbc. I am unable to compile jpf-symbc because of missing packages certain import statements do not work. I have used the mercurial links available for download for both jpf-core and jpf-symbc( http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc). Can anyone please help me fix the issue of jpf-symbc compilation? If jpf-core and jpf-symbc are incompatible, how do I know the compatible version of jpf-core for the available jpf-symbc? Any immediate help would be really helpful. Thanks and Regards, Anwesha |
|
From: Peter M. <Pet...@na...> - 2010-04-19 18:07:12
|
we are still getting subscriptions for the old sourceforge mailing lists. Please note that we have consolidated the mailing lists into one Google group on http://groups.google.com/group/java-pathfinder and update your subscriptions accordingly. Thanks, -- Peter |
|
From: Neha R. <neh...@gm...> - 2010-01-30 01:09:16
|
Hello Everyone, We are moving the mailing lists from the sourceforge to googlegroups. You can subscribe to the new mailing list at: http://groups.google.com/group/java-pathfinder/subscribe We are consolidating the developers and users mailing lists into a single list. This move is a part of moving JPF from sourceforge to a server at NASA Ames Research Center. *JPF continues to remain open source* with its different extensions now available as separate projects. As a reminder, details about downloading and installing JPF can be found on the new JPF wiki at: http://babelfish.arc.nasa.gov/trac/jpf We look forward to your continued participation and interest in JPF and its extensions. Cheers, Neha -- ------------------------------------------------- Neha Rungta Research Scientist Robust Software Engineering Group SGT/NASA Ames Research Center Moffett Field, CA 94035 -------------------------------------------------- |
|
From: Pasareanu, C. S. (ARC-TI)[S. G. T. I. (S. Inc.)] <cor...@na...> - 2009-11-13 04:37:08
|
Hi: symbc is being moved to the new repository. More info will be available soon. Corina ________________________________________ From: Akira Yoshihara [a-...@do...] Sent: Thursday, November 12, 2009 7:49 PM To: jav...@li... Subject: [Javapathfinder-devel] Where is symbc project in the new repository? Hi all, Would anyone be kind enough to tell me where the symbc (Symbolic Test Data Generation) project exist in the new repository server? It looks as if this project (or extension, formerly) has be removed from the project lists when JPF moved to this new server. Is it still under process of porting? Or do we have to manually reconstruct this extension so that it fits new project architecture, as referred to by the following link? http://babelfish.arc.nasa.gov/trac/jpf/wiki/FAQ#WhatdoIhavetodotoportmyoldextensiontothenewarchitecture Thank you very much and sincerely, Akira Yoshihara ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Javapathfinder-devel mailing list Jav...@li... https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel |
|
From: Akira Y. <a-...@do...> - 2009-11-13 02:07:38
|
Hi all, Would anyone be kind enough to tell me where the symbc (Symbolic Test Data Generation) project exist in the new repository server? It looks as if this project (or extension, formerly) has be removed from the project lists when JPF moved to this new server. Is it still under process of porting? Or do we have to manually reconstruct this extension so that it fits new project architecture, as referred to by the following link? http://babelfish.arc.nasa.gov/trac/jpf/wiki/FAQ#WhatdoIhavetodotoportmyoldextensiontothenewarchitecture Thank you very much and sincerely, Akira Yoshihara |
|
From: Neha R. <neh...@gm...> - 2009-10-30 20:30:56
|
Hello Everyone, As you all know the JPF location has moved to http://babelfish.arc.nasa.gov/trac/jpf Search engines still, however, bring up the sourceforge page. In an effort to point new and other existing users to the new JPF home we ask you to please update on your research and personal webpages the JPF links from sourceforge to the babelfish link shown above. And if you don't have a reference to JPF, this would be a great time to add one. We are hoping this will help in upping the google-juice and other search engines ranking scores for the new JPF home. Thanks, Neha -- ------------------------------------------------- Neha Rungta Research Scientist Robust Software Engineering Group SGT/NASA Ames Research Center Moffett Field, CA 94035 -------------------------------------------------- |
|
From: Peter M. <pet...@na...> - 2009-10-21 17:10:32
|
babelfish.arc.nasa.gov will be down on Friday 10/23 5pm, due to some infrastructure work. All should be back to normal on Monday 10/26 Sorry for the inconvenience -- Peter |
|
From: Peter M. <Pet...@na...> - 2009-10-07 17:49:00
|
Please have a look at our blog on
http://babelfish.arc.nasa.gov/trac/jpf/blog
to stay on top of JPF changes that might be of interest for you. The
idea is that everybody who adds documentation or changes code that
might be relevant to others posts a short note there
-- Peter
|
|
From: Peter M. <pet...@na...> - 2009-09-28 01:28:47
|
It is done - JPF has found its new home on:
http://babelfish.arc.nasa.gov/trac/jpf
JPF has moved to its own server that is hosted at the NASA Ames
Research Center. First and foremost - this does not change the
licensing or public read access. JPF continues to be open source.
The reason for this move was twofold:
(1) extensions have become so numerous that we need to split them into
their own projects (which can be hosted on the new server). JPF
extensions do not necessarily coexist, and not many people work with
more than one at a time, so they shouldn't convolute the JPF
distribution and fight for classpath priorities. Since we still want
to keep the jpf core and all our current extensions together, we
needed more than one repository for JPF. Now we have Mercurial
repositories for (eventually) each of them, all can be loaded as
separate projects into your favorite IDE. You can follow the status of
JPF projects (core and extensions) on http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/start
(2) JPF is increasingly used as a production tool, so its user
documentation becomes crucial. A wiki is much more suitable than the
old static website to keep things up-to-date and facilitate
collaborative development. The caveat is that we need strong
hierarchical navigation for the JPF docu. So we wanted to have control
over our wiki, and have chosen Trac so that we can integrate the docu
with issue management and (eventually) the Mercurial repositories.
Splitting core and extensions also required a new JPF configuration/
bootstrapping mechanism, which now uses site- and per-project
configuration files, in addition to the old default.properties and the
*.jpf application properties. Details on http://babelfish.arc.nasa.gov/trac/jpf/wiki/user/config
Speaking of *.jpf application properties - they are also the basis for
the new jpf-shell infrastructure, which finally unifies the plugins,
and uses standalone swing applications as graphical front ends of JPF
(while still being able to communicate with the Eclipse/NetBeans IDEs).
The Sourceforge repository will stay, i.e. people can choose when to
port their extensions. However, the JPF core in the Sourceforge
Subversion repository will not be updated anymore - be aware of that
code bases will diverge quickly, and our live site is now on http://babelfish.arc.nasa.gov/trac/jpf
.
Check out http://babelfish.arc.nasa.gov/trac/jpf/blog and the rest of
the (evolving) Wiki to find details about other technical and
distribution changes.
If you are a maintainer of a current JPF extension and need write
access for the new repositories or the Wiki, please go to http://babelfish.arc.nasa.gov/trac/jpf/wiki/about/account
and register for an account on the new server.
The new server does not (yet) have mailing lists, which means we will
keep the Sourceforge mailing lists open for the time being.
-- the JPF team
|
|
From: Pavel P. <pa...@ds...> - 2009-06-26 08:35:12
|
Hello, my name is Pavel Parizek. I am the main developer of the newly added extension "RTEmbed". The extension is aimed at verification of Java programs for real-time and embedded platforms, in particular (but not exclusively) of Java programs compliant with RTSJ. Currently, it includes a checker of RTSJ memory access rules and an optimization of state space traversal that is based on platform-specific restrictions of concurrency. The restrictions are described in P.Parizek and Tomas Kalibera. Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs, In FMICS 2009, LNCS, to appear. PDF of the paper is available at http://dsrg.mff.cuni.cz/publications/ParizekKalibera-RestrictConcurrency.pdf. In future, we plan to add support for other kinds of runtime errors introduced by RTSJ and to develop additional domain-specific optimizations of state space traversal. The extension is in the "rtembed" directory. Additional information on configuration and running are in the Readme file. With questions or bug reports, please contact me at pa...@ds.... Regards, Pavel -- Pavel Parizek, Ph.D. Researcher Distributed Systems Research Group http://dsrg.mff.cuni.cz/~parizek Phone: (+420) 2 2191 4235 Fax: (+420) 2 2191 4323 __________________________________ Department of Software Engineering Faculty of Mathematics and Physics Charles University in Prague Malostranske namesti 25 11800 Prague 1, Czech Republic |
|
From: Peter M. <Pet...@na...> - 2009-05-06 05:26:45
|
JPF has been nominated as a candidate for the NASA software of the year award, which would help us a lot with the things we have in mind for JPF's future. In order to make the next hurdle, we have to provide user testimonials (that are used NASA internally). If you feel inclined to do so, please send an informal paragraph or two to my email address, which is <pet...@na...> Thanks for supporting your (hopefully) favorite swiss army knife for Java verification -- Peter |
|
From: Michal K. <mic...@gm...> - 2009-04-03 13:22:22
|
Hi all, I would like to try the NetBeans plugin. So far I was able to run the 'RunJPF project' from NetBeans and I found a couple of new JPF icons in the toolbar but I don't how to use the plugin. Is there any readme? Thanks. --MK |
|
From: Neha R. <neh...@gm...> - 2009-03-31 16:42:47
|
Hi,
Attached is the PADTAD 2009 CFP. Please consider submitting to it and
participating.
Thanks,
Neha
=================================================================================
[Apologies for multiple copies]
Workshop on Parallel and Distributed Systems:
Testing, Analysis, and Debugging
(PADTAD - VII)
July 19-20, 2009
http://www.haifa.il.ibm.com/Workshops/padtad2009/index.shtml
In conjunction with
International Symposium on Software Testing and Analysis
(ISSTA 2009)
IMPORTANT DATES
====================================================================
Submission deadline: 19 April 2009
Author notification: 11 May 2009
Final version: 25 May 2009
PADTAD Workshop: 19-20 July 2009
GOALS & SCOPE OF WORKSHOP
====================================================================
The PADTAD 2009 workshop is a two days event at ISSTA 2009 focusing on
techniques and systems that aid in the testing, analysis, and
debugging of multi-threaded/parallel/distributed applications
systems. The workshop has a practical and applied emphasis on systems
that have been implemented in (at least) prototype form. The workshop
concentrates on works whose main contributions are in the field of
testing, debugging, and education.
Although debuggers and profilers are the traditional examples of
testing and debugging tools on sequential machines, there are issues
unique to concurrent systems that are not commonly addressed. Examples
of such significant challenges include deadlock, load imbalance, data
sharing patterns, race conditions, and contention. Established testing
techniques and tools are insufficient for non-sequential programs
because they largely ignore timing and scheduling which are inherent
in concurrent systems. Beyond the shortcomings on current tools and
technologies, the rising generating of programmers and designers need
to be more versed in concurrent systems design and programming.
Education and curriculum are critical to fully realizing the full
potential of multi-core technology as we need to begin training now
the students who will make multi-core happen in a large scale. As
such, we strongly encourage abstracts and regular papers devoted to
education and curriculum at all levels including pedagogy, exercises,
projects, experience reports, etc.
Following is a broad list of topics of interest to the workshop:
* Curriculum and education for multi-core design, programming,
testing, and analysis
* Techniques for multi-core processors
* Techniques for MPI and OpenMP or other library based
applications
* Transactional memory
* Tools for testing or debugging of
Multi-threaded/Parallel/Distributed applications
* Test generation algorithms for
Multi-threaded/Parallel/Distributed applications
* Debugging advanced network interface technologies (e.g.,
Myrinet, VIA)
* Debugging and testing Multi-threaded/Parallel/Distributed
applications
* Testing and Debugging of
Multi-threaded/Parallel/Distributed applications written
using domain-specific languages
* Using static analysis or formal verification to enhance
debugging and testing of
Multi-threaded/Parallel/Distributed applications
* Formal specification of concurrency libraries, and uses in
compliance testing of implementations
* Detecting race conditions and deadlocks
* Replay of Multi-threaded/Parallel/Distributed applications
* Finding timing bugs early in the process
* Testing real-time Multi-threaded/Parallel/Distributed
applications
* Fault injection of Multi-threaded/Parallel/Distributed
applications
* Testing the fault tolerance of
Multi-threaded/Parallel/Distributed applications
* Testing and debugging techniques for timing related bugs in
hardware
* Pilots in applying new testing techniques to
Multi-threaded/Parallel/Distributed applications
* Multi-threaded/Parallel/Distributed review techniques and
review tools
* Teaching of Multi-threaded/Parallel/Distributed system
design, verification and testing
Accepted papers, as well as education session abstracts, will be
published in a CD-ROM proceedings and will be included in the ACM
Digital Library.
TUTORIALS
====================================================================
Intel®'s Threading Building Blocks - a Shared Memory Parallel
Programming Library By Arch Robison, Senior Principal Engineer, Intel
Corporation
This tutorial is an introduction to Intel's Threading Building Blocks
(Intel's TBB), a commercially supported open-source C++ template
library for shared-memory parallel programming, notably for multi-core
processors. Though threads are a popular means of shared-memory
parallel programming, they are a low-level unstructured construct
whose undisciplined use can cause both correctness and performance
problems. This tutorial explains these problems and how TBB addresses
them, without resorting to special compilers or languages. The
tutorial will explain the architecture of TBB, its motivation, and how
to effectively apply TBB to problems by using parallel generic
programming. Attendees will get some hands on experience with TBB
Multicore Programming with Cilk++
By Pablo Halpern, Member of Technical Staff, Cilk Arts
This hands-on tutorial is an introduction to Cilk++, a faithful
extension of C++ into the multicore realm. The tutorial will introduce
key parallel programming concepts impacting performance and
reliability, and illustrate how to multicore-enable existing C++
applications using Cilk++. In a hands-on lab exercise featuring both
Linux GCC and Visual Studio environments, attendees will:
* Apply the Cilk++ keywords to expose parallelism in a sequential
application
* Use the Parallel Performance Analyzer to optimize the application
* Use the Cilkscreen Race Detector to identify race bugs
* Apply Cilk++ hyperobjects to eliminate data races on global
variables
ORGANIZATION
====================================================================
PADTAD General Chair:
* Ganesh Gopalakrishnan
University of Utah
PADTAD Program Chair
* Eitan Farchi
IBM Haifa Research Laboratory
PADTAD Community Chair
* Eric Mercer
Brigham Young University
PROGRAM COMMITTEE
====================================================================
* Eric Mercer, Brigham Young University, U.S.A
* Yosi Ben-Asher, Haifa University, Israel
* Giorgio Delzanno, Universita di Genova, Italy
* Jack Dongarra, University of Tennessee, U.S.A
* Eitan Farchi, IBM Haifa Research Lab, Israel
* Mike Feeley, University of British Columbia, Canada
* Bernd Finkbeiner, Universität des Saarlandes , Germany
* Cormac Flanagan, University of California, Santa Cruz, USA
* Ganesh Gopalakrishnan, University of Utah
* Klaus Havelund, NASA's Jet Propulsion Labratory
* Daniel J. Quinlan, Lawrence Livermore National Labratories, U.S.A
* Joao Lourenco, Univ. Nova de Lisboa, Portugal
* Zhiqiang Ma, Intel, U.S.A
* Paul Petersen, Intel U.S.A
* Shaz Qadeer, Microsoft Research, USA
* Madan Musuvathi, Microsoft Research, USA
* Grigore Rosu, University of Illinois at Urbana-Champaign, U.S.A
* Christoph Steindl, Catalysts, Austria
* Scott Stoller, SUNY, U.S.A
* Paul Strooper, University of Queensland, Australia
* Serdar Tasiran, Koç University, Turkey
* Shmuel Ur, IBM Haifa Research Lab, Israel
* Willem Visser, SEVEN Networks, U.S.A
* Tao Xie, North Carolina State University, U.S.A
* Matt Might, University of Utah, U.S.A.
* Rajeev Thakur, Argonne National Laboratory, U.S.A.
--
-------------------------------------------------
Neha Rungta
Research Assistant
Verification and Validation Lab
Brigham Young University
http://neharungta.com
--------------------------------------------------
|
|
From: Watcharin L. <wat...@us...> - 2009-03-13 04:46:11
|
Hello, My name is Watcharin. I am a developer of the newly added JPF extension "net-iocache". Net-iocache is an extension for verifying networked applications. JPF executes one of the processes in an application, whereas the others run on the standard Java virtual machine. Net-iocache captures inputs/outputs of the target program and replays them when the program needs again after backtracking. The algorithm to be run in Net-iocache is presented in C. Artho, W. Leungwattanakit, M. Hagiya, and Y. Tanabe. Efficient model checking of networked applications. In Proc. TOOLS EUROPE 2008, volume 19 of LNBIP, pages 22–40, Zurich, Switzerland, 2008. Springer. For any information or to report problems, please contact: Watcharin Leungwattanakit: wat...@is... Regards, Watcharin Leungwattanakit |
|
From: Taehoon L. <ta...@ky...> - 2009-03-04 03:04:17
|
Hi doc/link.html has erratum. A patch is attached. ------------------------------------------------------------------------------------------------------------------ <li><a href="ht<script src="http://www.google-analytics.com/urchin.js" type="text/javascript"> </script> <script type="text/javascript"> _uacct = "UA-686208-1"; urchinTracker(); </script>tp://secure.ucd.ie/products/opensource/ESCJava2/">ESC/Java 2 - the Extended Static Checker for Java</a></li> ------------------------------------------------------------------------------------------------------------------ <li><a href="http://secure.ucd.ie/products/opensource/ESCJava2/">ESC/Java 2 - the Extended Static Checker for Java</a></li> |
|
From: Michal K. <mic...@gm...> - 2009-01-11 20:45:50
|
Hi,
it sounds good. Thank you!
MK
Mateusz Ujma wrote:
> Hi,
>
> I did some debbuging and here what I've got.
>> I think the state of VM before the division is invoked should be the
>> same in both cases. Am I right or not?
>>
> Yes you are right the state is the same. I've checked that by adding
> some code into NativePeer.executeMethod() which is invoked for example
> when JPF finds
> "System.out.println("divide");". But after learning that, I get
> confused, because I thought if the state has been seen already seen, JPF
> should not execute
> any more code on that path. I did some more debugging and that's why it
> executes all the code:
> After printing first "divide" JPF backtracks to "int x =
> Verify.getInt(1, 2); ". And starts to execute this code, execution of
> this code is done in ThreadInfo.executeStep method.
> This method executes code until there is no instruction left. So when
> JPF steps into ThreadInfo.executeStep it will execute int x =
> Verify.getInt(1, 2); and then move to System.out.println("divide");.
> The state information will not be used because state comparision is done
> in higher level than ThreadInfo.executeStep.
>
> I hope I was clear and the most important I didn't write untrue
> information.
>
> Yours sincerely
>
> Mateusz Ujma
>
> Michal Kebrt pisze:
>> Hi,
>>
>> I have the following JUnit test executed under JPF.
>>
>> public class MathTest {
>> @Test
>> public void add() {
>> System.out.println("add");
>> int x = Verify.getInt(1, 2);
>> }
>>
>> @Test
>> public void divide() throws Exception {
>> System.out.println("divide");
>> }
>> }
>>
>> And I'm curious why the second test 'divide' is run twice. Firstly I
>> thought it's clear, the 'add' test generates two values in the
>> variable 'x' so the division will be invoked twice as well. But later
>> I realized that x is a local variable that shouldn't affect the rest
>> of the class. I think the state of VM before the division is invoked
>> should be the same in both cases. Am I right or not?
>>
>> Thanks
>>
>> Michal
>>
>> ------------------------------------------------------------------------------
>>
>> Check out the new SourceForge.net Marketplace.
>> It is the best place to buy or sell services for
>> just about anything Open Source.
>> http://p.sf.net/sfu/Xq1LFB
>> _______________________________________________
>> Javapathfinder-devel mailing list
>> Jav...@li...
>> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
>>
>>
>
|
|
From: Mateusz U. <mat...@gm...> - 2009-01-11 20:23:14
|
Hi,
I did some debbuging and here what I've got.
> I think the state of VM
> before the division is invoked should be the same in both cases. Am I right or not?
>
Yes you are right the state is the same. I've checked that by adding
some code into NativePeer.executeMethod() which is invoked for example
when JPF finds
"System.out.println("divide");". But after learning that, I get
confused, because I thought if the state has been seen already seen, JPF
should not execute
any more code on that path. I did some more debugging and that's why it
executes all the code:
After printing first "divide" JPF backtracks to "int x =
Verify.getInt(1, 2); ". And starts to execute this code, execution of
this code is done in ThreadInfo.executeStep method.
This method executes code until there is no instruction left. So when
JPF steps into ThreadInfo.executeStep it will execute int x =
Verify.getInt(1, 2); and then move to System.out.println("divide");.
The state information will not be used because state comparision is done
in higher level than ThreadInfo.executeStep.
I hope I was clear and the most important I didn't write untrue information.
Yours sincerely
Mateusz Ujma
Michal Kebrt pisze:
> Hi,
>
> I have the following JUnit test executed under JPF.
>
> public class MathTest {
> @Test
> public void add() {
> System.out.println("add");
> int x = Verify.getInt(1, 2);
> }
>
> @Test
> public void divide() throws Exception {
> System.out.println("divide");
> }
> }
>
> And I'm curious why the second test 'divide' is run twice. Firstly I thought
> it's clear, the 'add' test generates two values in the variable 'x' so the
> division will be invoked twice as well. But later I realized that x is a local
> variable that shouldn't affect the rest of the class. I think the state of VM
> before the division is invoked should be the same in both cases. Am I right or not?
>
> Thanks
>
> Michal
>
> ------------------------------------------------------------------------------
> Check out the new SourceForge.net Marketplace.
> It is the best place to buy or sell services for
> just about anything Open Source.
> http://p.sf.net/sfu/Xq1LFB
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
>
>
|
|
From: Taehoon L. <ta...@ky...> - 2009-01-10 20:09:12
|
Hi
I need to store a instruction of path.
for example
int a= random();
if(a<0){
a=a/10;
}else {
a=a+10;
}
this program has two execution paths.
I need to store each path of program. and store possible value of variable.
I think similar listener is already implemented.
Can you tell me where is it?
--
------------------------------------------------------
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-10-8932-2732
EMAIL: ta...@ky...
-------------------------------------------------------
|
|
From: Michal K. <mic...@gm...> - 2009-01-09 09:12:31
|
Hi,
I have the following JUnit test executed under JPF.
public class MathTest {
@Test
public void add() {
System.out.println("add");
int x = Verify.getInt(1, 2);
}
@Test
public void divide() throws Exception {
System.out.println("divide");
}
}
And I'm curious why the second test 'divide' is run twice. Firstly I thought
it's clear, the 'add' test generates two values in the variable 'x' so the
division will be invoked twice as well. But later I realized that x is a local
variable that shouldn't affect the rest of the class. I think the state of VM
before the division is invoked should be the same in both cases. Am I right or not?
Thanks
Michal
|
|
From: Michal K. <mic...@gm...> - 2008-12-02 22:06:17
|
Hi,
I encountered NPE in the Instruction class when calling
ChoiceGenerator.getInsn().getSourceLine() and when source is not found on the
line: Source src = Source.getSource(file);
Fix should be easy:
Source src = Source.getSource(file);
if (src != null) {
String srcLine = src.getLine(line);
if (srcLine != null) {
return srcLine;
}
}
return "(" + file + ":" + line + ")";
Michal Kebrt
|
|
From: Peter C. M. <Pet...@na...> - 2008-11-20 23:53:29
|
unless I hear back from you, I'm considering to change the defaults.properties and *.jpf format to only use ',' as a list separator. The problem is that - ':' doesn't work for Windows paths - ' ' doesn't work for both Unix and Windows paths - ';' doesn't work if you have to specify Java signatures That leaves us with the ' ', unless we introduce tons of different Config.getStringArray()/getPathStringArray()/getSignatureArray()... methods, or specify the delimiter pattern as a getStringArray() parameter (which is also bad because that opens the door to tons of inconsistent clients) . It seems much better to use one platform independent format for everything. ?? DOES ANYBODY KNOW A CASE WHERE ',' WOULD NOT WORK AS A LIST SEPARATOR ?? If so, please speak up Thanks, -- Peter |
|
From: Peter C. M. <Pet...@na...> - 2008-11-18 03:21:49
|
Not sure I understand the problem - vm.peer.packages is an ordered list, i.e. you can control which packages are tried first during NativePeer lookup -- Peter On Nov 11, 2008, at 12:54 PM, Mateusz Ujma wrote: > 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: Michal K. <mic...@gm...> - 2008-11-17 17:09:13
|
Hi, I'm not sure whether this is the case of vm.sourcepath. Just look at ClassInfo.java:1458. It would be nice to be able to include jars in vm.sourcepath. Michal Sandro Badame wrote: > Hi Michal, > > I'm not sure if I'm allowed to answer here or not, but I'm pretty > confident in my quick naive answer: Yes. In fact it's common to > env_jpf.jar included in the classpath. > > --Sandro > > Michal Kebrt wrote: >> Hi, >> >> may vm.classpath and vm.sourcepath contain paths to jar files? >> >> 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: Adam K. <ak...@cs...> - 2008-11-17 14:58:40
|
Hi, This is to present to you a new extension to JPF, concolic execution, and a fuzzing tool built on the extension, jFuzz. The goal is to create effective test inputs for programs that read (binary or text) files. The concolic extension can be used separately from jFuzz and used for other purposes. In short, during concolic execution, the program runs as usual but also keeps track of the precise way the inputs influences the control path. The result is a logical fomula, path condition, that describes the input and, importantly, the set of all inputs that would drive the program execution along the same control-flow path. Concolic execution is similar to symbolic execution in that it collects constraints and marks inputs as symbolic, but concolic execution is different in that the original program execution is not affected, the exact same concrete values are used, and that only 1 execution path is taken (as opposed to the whole execution tree in symbolic execution). jFuzz is a fuzzer build on concolic execution. It's goal is to create program inputs (files) that exercise many distinct execution path in the program under test. jFuzz works by running JPF in concolic mode many times. First time jFuzz runs, it collects the path condition. Then, jFuzz negates each path of the path condition systematically, and by solving them using a constraint sover, jFuzz creates additional program inputs, each designed to exercise a unique path. The code is in the 'concolic' source folder. The Readme.html in that folder gives additional information. The readme is duplicated here http://people.csail.mit.edu/dharv/jfuzz/ Over the next months, we will work on improvements to concolic and jFuzz: caching for constraints, input selection heuristics and parallelization. If you're interested in helping out - write me an email (ak...@cs...) The concolic extension and jFuzz were developed by David Harvison and Adam Kiezun at MIT, with guidance from Corina Pasareanu and Peter Dillinger from NASA. ./adam |
