Menu
▾
▴
javapathfinder-user — usage related topics (installing, running, options, output...)
You can subscribe to this list here.
| 2005 |
Jan
|
Feb
|
Mar
|
Apr
(3) |
May
(5) |
Jun
(2) |
Jul
(9) |
Aug
(7) |
Sep
(4) |
Oct
(7) |
Nov
(20) |
Dec
(5) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2006 |
Jan
(1) |
Feb
(8) |
Mar
(17) |
Apr
(25) |
May
(7) |
Jun
(1) |
Jul
|
Aug
(1) |
Sep
(14) |
Oct
(5) |
Nov
(1) |
Dec
(5) |
| 2007 |
Jan
(7) |
Feb
(3) |
Mar
|
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
(4) |
Sep
(8) |
Oct
(7) |
Nov
(2) |
Dec
(11) |
| 2008 |
Jan
(1) |
Feb
(9) |
Mar
(3) |
Apr
(8) |
May
(2) |
Jun
(6) |
Jul
(5) |
Aug
(13) |
Sep
(2) |
Oct
(7) |
Nov
(3) |
Dec
(28) |
| 2009 |
Jan
(10) |
Feb
(19) |
Mar
(12) |
Apr
(10) |
May
|
Jun
(1) |
Jul
|
Aug
(1) |
Sep
(2) |
Oct
(3) |
Nov
|
Dec
|
| 2010 |
Jan
(1) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2015 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
|
Dec
|
|
From: Samuel B. <sam...@gm...> - 2015-10-12 18:00:57
|
Hello,
I am a PhD student at Brazil and am currently using JPF on my doctoral work.
I have a question about JPF: do you know any resource on JPF that allows
model checking infinitely recursive programs? Theoretically the
verification of these programs would never finish, but wouldn't it be
possible to model check them in a finite time?
Ex:
*import gov.nasa.jpf.vm.Verify;public class ProcessVerify { public
static void infiniterec () { int inf = Verify.getInt(0, 1);
System.out.println ("inf == " + inf); infiniterec2 (); }
public static void infiniterec2 () { int inf2 = Verify.getInt(0,
1); System.out.println ("inf2 == " + inf2); infiniterec
(); } public static void main (String [] args) {
infiniterec(); }}*
How could we model check the previous program in a finite time? Do you know
how to do that?
Best,
|
|
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: Corina P. <Cor...@na...> - 2010-03-24 17:28:32
|
prateek sinha wrote: > Does JPF forms the Kripke Structure of a given Java byte code . If yes , in > which file is it stored > > Hi: JPF does not build a Kripke structure explicitly: it explores the Java program on the fly (and it stores the explored program states). -- Corina Pasareanu, PhD CMU/NASA Ames http://ti.arc.nasa.gov/profile/pcorina/ |
|
From: prateek s. <pra...@gm...> - 2010-03-24 16:06:00
|
Does JPF forms the Kripke Structure of a given Java byte code . If yes , in which file is it stored -- Regards, Prateek Kumar Sinha CSE , Final Year MNNIT , Allahabad |
|
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: Neha R. <neh...@gm...> - 2009-10-30 22:37:16
|
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:33
|
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 02:18:56
|
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: Anthony A. <aa...@cs...> - 2009-09-15 03:06:20
|
Hello all,
I do hope this is the appropriate forum for sending out a question. If
not, please accept my sincerest apologies. I have posted in the
SourceForge forum but it looks quite tranquil there.
When running JPF against a set of dynamically spawning Thread
subclasses, I receive a java.lang.ArrayStoreException assigning a
variable declared as int to an initialized object-level array of ints.
I'm not sure how this is possible. When I run the code outside of JPF
I never receive this exception. Even stranger, under JPF the line
executes several times successfully and then fails with this
exception. All of this is sequential, taking place in a single thread.
Is there anything anyone is aware of that JPF might be doing to
conceivably attempt to assign a non-integer value here, when the
variable on the right of the assignment is explicitly (and locally)
declared int? I'm utterly at a loss about this.
I would heartily appreciate any insight anyone has on this. The code
in question is as follows:
public int[] fire(int[] m, int e) {
int[] n = m.clone();
for(int z: n) System.out.println("[ -> " + z);
System.out.println("------");
int i;
int t = getTransition(e);
if(t == -1) return null;
for(i = 0; i < arcs[t][0].length; i++) {
n[arcs[t][0][i][0]] -= arcs[t][0][i][1]; // *** ArrayStoreException
occurs *here* ***
if(n[arcs[t][0][i][0]] < 0)
return null;
}
for(i = 0; i < arcs[t][1].length; i++)
n[arcs[t][1][i][0]] += arcs[t][1][i][1];
return n;
}
|
|
From: Arnab De <arn...@gm...> - 2009-08-27 14:09:03
|
Hi, I installed JPF from SVN today (27th Aug). I can build it and run from the root directory, but when I try to run it from some different directory (for example build/examples) it gives the following error. $../../bin/jpf +vm.classpath=. Racer [WARNING] orphant NativePeer method: java.lang.ClassLoader.init0()V [WARNING] orphant NativePeer method: java.lang.ClassLoader.getResourcePath(Ljava/lang/String;)Ljava/lang/String; [WARNING] orphant NativePeer method: java.lang.Thread.setDaemon0(Z)V [WARNING] orphant NativePeer method: java.lang.Thread.setName0(Ljava/lang/String;)V [WARNING] orphant NativePeer method: java.lang.Thread.init0(Ljava/lang/ThreadGroup;Ljava/lang/Runnable;Ljava/lang/String;J)V [WARNING] orphant NativePeer method: java.lang.System.createSystemOut()Ljava/io/PrintStream; [WARNING] orphant NativePeer method: java.lang.System.createSystemErr()Ljava/io/PrintStream; [WARNING] orphant NativePeer method: java.lang.System.getKeyValuePairs()[Ljava/lang/String; [SEVERE] error during VM runtime initialization: wrong model classes (check vm.[boot]classpath) Also, I cannot build it with eclipse (version 3.2). Please tell me if I'm making some mistake. I'm using Java 1.6. Thanks and regards, Arnab -- Arnab De ----------------------------------------------------------- Graduate Student. Computer Science and Automation Department, Indian Institute of Science, Bangalore. http://arnabde03.googlepages.com/ ----------------------------------------------------------- |
|
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: 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: ZHU H. <ry...@us...> - 2009-03-08 16:34:50
|
Dear Sir or madam,
I tried the example under "~/trunk/extensions/symbc/examples/coverage"
this week to see how the symbolic execution runs.
As it is said that "The trickiest part here is
CheckCoverage.processTestCase()". But what I got from the symbolic
execution is like this:
Property Violated: PC is # = 3
int_2_SYMINT[-10000] < CONST_5 &&
int_1_SYMINT[-10000] < CONST_0 &&
(int_2_SYMINT[-10000] + int_1_SYMINT[-10000]) <= CONST_0
Property Violated: result is
"java.lang.reflect.InvocationTargetException: in
coverage.CheckCoverage.processTestCase :
java.lang.NullPointerException..."
****************************
====================================================== error #8
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.reflect.InvocationTargetException: in
coverage.CheckCoverage.processTestCase : java.lang.NullPointerException
at coverage.CheckCoverage.processTestCase(Native Method)
at
coverage.MyClassWithPathAnnotations.myMethod(MyClassWithPathAnnotations.java:34)
at
coverage.MyDriverForPathAnnotations.main(MyDriverForPathAnnotations.java:7)
====================================================== trace #8
------------------------------------------------------ transition #0
thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>main}
[487 insn w/o sources]
------------------------------------------------------ transition #1
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..0,delta=+1,cur=0]
[15 insn w/o sources]
------------------------------------------------------ transition #2
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..1,delta=+1,cur=1]
[4 insn w/o sources]
------------------------------------------------------ transition #3
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..1,delta=+1,cur=0]
[4 insn w/o sources]
------------------------------------------------------ transition #4
thread: 0
gov.nasa.jpf.symbc.numeric.PCChoiceGenerator[0..1,delta=+1,cur=1]
[4 insn w/o sources]
====================================================== Method Summaries
myMethod(-1,2) --> "java.lang.reflect.InvocationTargetException: in
coverage.CheckCoverage.processTestCase :
java.lang.NullPointerException..."
...
...
Here is my platform infos:
Linux 2.6.22-14-server #1 SMP Tue Feb 12 03:10:53 UTC 2008 x86_64 GNU/Linux
java version "1.6.0_07"
Java(TM) SE Runtime Environment (build 1.6.0_07-b06)
Java HotSpot(TM) 64-Bit Server VM (build 10.0-b23, mixed mode)
And my jpf.properties:
vm.classpath = .
vm.sourcepath+= ,${user.home}/tmp
vm.storage.class=
symbolic.method=myMethod(sym#sym)
search.multiple_errors=true
jpf.report.console.finished=
coverage.MyDriverForPathAnnotations
vm.insn_factory.class = gov.nasa.jpf.symbc.SymbolicInstructionFactory
jpf.listener = gov.nasa.jpf.symbc.SymbolicListener
log.level=warning
I typed this command:
:~/trunk/extensions/symbc/examples$ ~/trunk/bin/jpf -c
coverage/jpf.properties coverage.MyDriverForPathAnnotations
I really don't how to get through this. The trickest
CheckCoverage.processTestCase() is what I am interested in. Would you
please tell me what's going on with the error I got?
Thank you.
Best regards
ZHU Hua
|
|
From: Hamasaki D. <dis...@so...> - 2009-02-28 10:06:44
|
New Orrgasm Enhancer Explain all i am and all i want. And i shouldn't the second table. The family were not at home. It, owing to the dense vegetation near the waterrather the country might afford. we started from santa understand god in the least degree, as well as. |
|
From: ZHU H. <ry...@us...> - 2009-02-23 14:47:28
|
Dear Sir or madam, I tried the example in http://javapathfinder.sourceforge.net/sw_model_checking.html I typied "java gov.nasa.jpf.JPF Rand_test" and "bin\jpf Rand_test", both came to an error like this: F:\HKUST\recrash\jpf>java gov.nasa.jpf.JPF Rand_test java.lang.UnsatisfiedLinkError: sun.misc.Unsafe.registerNatives (no peer) at sun.misc.Unsafe.<clinit>(sun\misc\Unkown:0) at java.util.concurrent.atomic.AtomicLong.<clinit>(java\util\concurrent\ atomic\Unkown:0) at java.util.Random.<init>(java\util\Unkown:10) at Rand_test.main(Rand_test.java:5) ----------------------------------- path to error (length: 1) Transition #0 Thread #0 Rand_test.java:5 Random random = new Random(42); // (1) [no source for: java\util\Unkown] [no source for: java\lang\Object.java] [no source for: java\util\Unkown] [no source for: java\util\concurrent\atomic\Unkown] [no source for: sun\misc\Unkown] ------------------------------------ end error path ------------------------------------ thread stacks Thread: main at sun.misc.Unsafe.<clinit>(sun\misc\Unkown:0) at java.util.concurrent.atomic.AtomicLong.<clinit>(java\util\concurrent\ atomic\Unkown:0) at java.util.Random.<init>(java\util\Unkown:10) at Rand_test.main(Rand_test.java:5) ------------------------------------ end thread stacks =================================== 1 Error Found: uncaught exception =================================== Is the problem caused by the lack of the libraries? How can I fix this? Thank you. Best regards ZHU Hua |
|
From: jiangfan s. <jia...@gm...> - 2009-01-22 20:34:16
|
Thanks very much, Corina. I would like to read this paper again more carefully first, modify my procedure to extend the JPF-SE to support array in my last email, and then send it back to you to check if the procedure is right or not. Best, Jiangfan On Thu, Jan 22, 2009 at 1:56 PM, Corina Pasareanu < Cor...@na...> wrote: > Hello: > > I assume you want to add array support in Symbolic JPF (i.e. JPF's symbc > extension). > That would be a good thing to do :) > For a start, you may want to take a look at the following paper, that > describes briefly the array support in our old version of symbolic > execution: > > Verification of Java Programs using Symbolic Execution and Invariant > Generation <http://ti.arc.nasa.gov/m/profile/pcorina/papers/spin04.ps>, > /Corina S. Pasareanu, Willem Visser/, in Proceedings of the the 11th > International SPIN Workshop on Model Checking of Software, 2004. > > With the techniques described above, you don't need array logic support in > the decision procedure. > > Best regards, > Corina > > > jiangfan shi wrote: > >> Hello, Corina, >> >> I am trying to add a very heuristic support for the array type due to my >> research requirement. I found there is a package named >> gov.nasa.jpf.symbolic.array, which includes some array related classes, such >> as ArrayIntStructure.java, ArrayBoolStructure.java. >> >> I have two understandings here, and I wonder if they are right or not. >> >> 1. The ArrayIntStructure class is a symbolic representation of >> array type via a vector, and it fulfills an array logic >> including read and write axioms, via to its' associated >> operations including set and get methods. >> 2. What I need to do for supporting array in JPF is the following: >> * call ArrayIntStructure constructor to do an array type >> initialization from the execute() method of >> BytecodesUtils.java * for every operators, such as >> add, minus, load, ifle etc., >> I need to check if an operand is an array type, and if so, >> call set or get methods in ArrayIntStructure class. >> * finally I need to transform some array-related path >> conditions to the format which is consistent with cvc3 or >> other decision procedures supporting array logic. I should >> do this in the SymbolicConstraintsGeneral class. >> Am I right for these two understandings? >> >> Thanks in advance, and any hint is highly appreciated! >> >> Jiangfan >> >> ------------------------------------------------------------------------ >> >> >> ------------------------------------------------------------------------------ >> This SF.net email is sponsored by: >> SourcForge Community >> SourceForge wants to tell your story. >> http://p.sf.net/sfu/sf-spreadtheword >> ------------------------------------------------------------------------ >> >> _______________________________________________ >> Javapathfinder-user mailing list >> Jav...@li... >> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user >> >> > > > -- > Corina Pasareanu, PhD > CMU/NASA Ames > http://ti.arc.nasa.gov/profile/pcorina/ > |
|
From: Corina P. <Cor...@na...> - 2009-01-22 19:57:06
|
Hello: I assume you want to add array support in Symbolic JPF (i.e. JPF's symbc extension). That would be a good thing to do :) For a start, you may want to take a look at the following paper, that describes briefly the array support in our old version of symbolic execution: Verification of Java Programs using Symbolic Execution and Invariant Generation <http://ti.arc.nasa.gov/m/profile/pcorina/papers/spin04.ps>, /Corina S. Pasareanu, Willem Visser/, in Proceedings of the the 11th International SPIN Workshop on Model Checking of Software, 2004. With the techniques described above, you don't need array logic support in the decision procedure. Best regards, Corina jiangfan shi wrote: > Hello, Corina, > > I am trying to add a very heuristic support for the array type due to > my research requirement. I found there is a package named > gov.nasa.jpf.symbolic.array, which includes some array related > classes, such as ArrayIntStructure.java, ArrayBoolStructure.java. > > I have two understandings here, and I wonder if they are right or not. > > 1. The ArrayIntStructure class is a symbolic representation of > array type via a vector, and it fulfills an array logic > including read and write axioms, via to its' associated > operations including set and get methods. > 2. What I need to do for supporting array in JPF is the following: > * call ArrayIntStructure constructor to do an array type > initialization from the execute() method of > BytecodesUtils.java > * for every operators, such as add, minus, load, ifle etc., > I need to check if an operand is an array type, and if so, > call set or get methods in ArrayIntStructure class. > * finally I need to transform some array-related path > conditions to the format which is consistent with cvc3 or > other decision procedures supporting array logic. I should > do this in the SymbolicConstraintsGeneral class. > > Am I right for these two understandings? > > Thanks in advance, and any hint is highly appreciated! > > Jiangfan > > ------------------------------------------------------------------------ > > ------------------------------------------------------------------------------ > This SF.net email is sponsored by: > SourcForge Community > SourceForge wants to tell your story. > http://p.sf.net/sfu/sf-spreadtheword > ------------------------------------------------------------------------ > > _______________________________________________ > Javapathfinder-user mailing list > Jav...@li... > https://lists.sourceforge.net/lists/listinfo/javapathfinder-user > -- Corina Pasareanu, PhD CMU/NASA Ames http://ti.arc.nasa.gov/profile/pcorina/ |
|
From: jiangfan s. <jia...@gm...> - 2009-01-22 18:19:56
|
Hello, Corina,
I am trying to add a very heuristic support for the array type due to my
research requirement. I found there is a package named
gov.nasa.jpf.symbolic.array, which includes some array related classes, such
as ArrayIntStructure.java, ArrayBoolStructure.java.
I have two understandings here, and I wonder if they are right or not.
1. The ArrayIntStructure class is a symbolic representation of array type
via a vector, and it fulfills an array logic including read and write
axioms, via to its' associated operations including set and get methods.
2. What I need to do for supporting array in JPF is the following:
- call ArrayIntStructure constructor to do an array type
initialization from the execute() method of BytecodesUtils.java
- for every operators, such as add, minus, load, ifle etc., I need to
check if an operand is an array type, and if so, call set or get
methods in
ArrayIntStructure class.
- finally I need to transform some array-related path conditions to
the format which is consistent with cvc3 or other decision procedures
supporting array logic. I should do this in the
SymbolicConstraintsGeneral
class.
Am I right for these two understandings?
Thanks in advance, and any hint is highly appreciated!
Jiangfan
|
|
From: Peter C. M. <Pet...@na...> - 2009-01-07 21:14:52
|
you have access to the code, the constpool, local var names and handler blocks, so you could re-engineer sources. However, normal execution mode is not very effective for this - you don't want traces but the complete control flow of a method. You could build the CFG by a different interpreter mode though (branching over ifs etc.) -- Peter On Jan 7, 2009, at 12:58 PM, Mido wrote: > Implementing VMListener, allows me to get a trace of the executed > byte code > instructions. > Is it possible to obtain the corresponding Java source-code of the > executed > byte code similar to what JAD does? > > Thanks. |
|
From: Mido <mid...@gm...> - 2009-01-07 20:59:02
|
Implementing VMListener, allows me to get a trace of the executed byte code instructions. Is it possible to obtain the corresponding Java source-code of the executed byte code similar to what JAD does? Thanks. |
|
From: Pasareanu, C. S. (ARC-TI)[S. G. T. INC.] <Cor...@na...> - 2009-01-07 20:46:10
|
the reason is we do not handle Strings yet. Corina Pasareanu, PhD http://ase.arc.nasa.gov/people/pcorina/ -----Original Message----- From: jiangfan shi [mailto:jia...@gm...] Sent: Wed 1/7/2009 1:28 PM To: jav...@li... Subject: [Javapathfinder-user] one question about symbolic execution overloop Hi, All, I encountered a problem with the symbolic execution package inside the jpf. I show the problem with the following example. I have a code like this: package jpftest; public class B { void test2(String str1){ for(int i=0;i<str1.length();i++) System.out.println(str1+i); } public static void main(String args[]){ B b=new B(); b.test2("hello"); } } I ran JPF with the following options: -c ../../../default.properties +vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory +jpf.listener=gov.nasa.jpf.symbc.HeapSymbolicListener +symbolic.dp=choco +symbolic.method=test2(sym) jpftest.B I got the outputs from JPF as following: symbolic.dp=choco Symbolic Execution Mode ---->Heap Listener JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center ====================================================== system under test application: jpftest\B.java ====================================================== search started: 09-1-7 ??1:23 Execute symbolic INVOKEVIRTUAL: test2(Ljava/lang/String;)V ( str1_1_SYMREF ) hello0 hello1 hello2 hello3 hello4 PC # = 0 Heap PC # = 0 Effect is # = 1 B:this == B:#271 **************************** ====================================================== Method Summaries No path conditions for test2(java.lang.String@272) ====================================================== Method Summaries (HTML) <h1>Test Cases Generated by Symbolic Java Path Finder for test2 (Path Coverage) </h1> No path conditions for test2(java.lang.String@272) ====================================================== results no errors detected ====================================================== statistics elapsed time: 0:00:01 states: new=2, visited=0, backtracked=1, end=1 search: maxDepth=1, constraints=0 choice generators: thread=1, data=1 heap: gc=2, new=289, free=32 instructions: 2984 max memory: 4MB loaded code: classes=68, methods=993 ====================================================== search finished: 09-1-7 ??1:23 The question is that why there is no path condition? I assume for a "for loop" there should be infinite paths, or with a depth threshold option there should be some paths. But from the output, I did not see any path condition. Did I miss some options to handle the loop specially, or someelse I should take care of? Thanks in advance for your help! Jiangfan ------------------------------------------------------------------------------ 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-user mailing list Jav...@li... https://lists.sourceforge.net/lists/listinfo/javapathfinder-user |
|
From: jiangfan s. <jia...@gm...> - 2009-01-07 19:29:08
|
Hi, All,
I encountered a problem with the symbolic execution package inside the
jpf. I show the problem with the following example.
I have a code like this:
package jpftest;
public class B {
void test2(String str1){
for(int i=0;i<str1.length();i++)
System.out.println(str1+i);
}
public static void main(String args[]){
B b=new B();
b.test2("hello");
}
}
I ran JPF with the following options:
-c ../../../default.properties
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+jpf.listener=gov.nasa.jpf.symbc.HeapSymbolicListener
+symbolic.dp=choco
+symbolic.method=test2(sym)
jpftest.B
I got the outputs from JPF as following:
symbolic.dp=choco
Symbolic Execution Mode
---->Heap Listener
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: jpftest\B.java
====================================================== search started:
09-1-7 下午1:23
Execute symbolic INVOKEVIRTUAL: test2(Ljava/lang/String;)V ( str1_1_SYMREF )
hello0
hello1
hello2
hello3
hello4
PC # = 0
Heap PC # = 0
Effect is # = 1
B:this == B:#271
****************************
====================================================== Method Summaries
No path conditions for test2(java.lang.String@272)
====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic Java Path Finder for test2 (Path
Coverage) </h1>
No path conditions for test2(java.lang.String@272)
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 0:00:01
states: new=2, visited=0, backtracked=1, end=1
search: maxDepth=1, constraints=0
choice generators: thread=1, data=1
heap: gc=2, new=289, free=32
instructions: 2984
max memory: 4MB
loaded code: classes=68, methods=993
====================================================== search
finished: 09-1-7 下午1:23
The question is that why there is no path condition? I assume for a
"for loop" there should be infinite paths, or with a depth threshold
option there should be some paths. But from the output, I did not see
any path condition.
Did I miss some options to handle the loop specially, or someelse I
should take care of?
Thanks in advance for your help!
Jiangfan
|
|
From: Lindel C. <spi...@ks...> - 2008-12-23 13:24:36
|
Catch your Christmaas present! http://cid-bae24fef32d336b6.spaces.live.com/blog/cns!BAE24FEF32D336B6!106.entry Of bodies one after another. He attains to thousands i leave this frail existence, when i lay this hue and slender waist then performed her ablutions. A swarm of breadandbutter misses? One wit suggested of ever rising to such a height of roughness,. |
|
From: Dunkelberger W. <da...@er...> - 2008-12-18 17:40:55
|
New Christmas pleasure :)) http://cid-c857c9b0f317964d.spaces.live.com/blog/cns!C857C9B0F317964D!106entry Plan for opening, 428. , intelligence respecting, but which, by its fine proportions, showed distinctly at no additional cost, fee or expense, a copy not test? Yes, i know but theyre all right i laid up at the age of fortyfive, sick of men, he said,. |
68 messages has been excluded from this view by a project administrator.
