Menu
▾
▴
javapathfinder-svn — source repository related messages (SVN)
You can subscribe to this list here.
| 2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(16) |
Jun
(42) |
Jul
(46) |
Aug
(48) |
Sep
(33) |
Oct
(26) |
Nov
(28) |
Dec
(38) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2009 |
Jan
(35) |
Feb
(80) |
Mar
(112) |
Apr
(108) |
May
(102) |
Jun
(126) |
Jul
(89) |
Aug
(82) |
Sep
(36) |
Oct
(7) |
Nov
(1) |
Dec
(4) |
| 2010 |
Jan
(87) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <sj...@us...> - 2008-06-30 20:59:04
|
Revision: 891
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=891&view=rev
Author: sjp100
Date: 2008-06-30 13:58:52 -0700 (Mon, 30 Jun 2008)
Log Message:
-----------
official cvc3 jni libraries and test code
Added Paths:
-----------
trunk/extensions/symbc/cvc3.jar
trunk/extensions/symbc/cvc3test.jar
trunk/extensions/symbc/libcvc3.jar
trunk/extensions/symbc/libcvc3.so
trunk/extensions/symbc/libcvc3jni.so
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-30 20:49:20
|
Revision: 890
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=890&view=rev
Author: pcorina
Date: 2008-06-30 13:49:07 -0700 (Mon, 30 Jun 2008)
Log Message:
-----------
Added symbc/env/jpf/java/lang/Math.java model class to handle "simple" math functions in symbolic execution mode.
!!!
To use and compile it (in eclipse) you should add:
symbc/env/jpf to jpf project source roots (BuildPath dialog).
!!!
Modified Paths:
--------------
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_Math.java
Added Paths:
-----------
trunk/extensions/symbc/env/jpf/
trunk/extensions/symbc/env/jpf/java/
trunk/extensions/symbc/env/jpf/java/lang/
trunk/extensions/symbc/env/jpf/java/lang/Math.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-30 20:01:21
|
Revision: 889
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=889&view=rev
Author: pcmehlitz
Date: 2008-06-30 13:01:19 -0700 (Mon, 30 Jun 2008)
Log Message:
-----------
* Math.log10 missing in native peer
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sj...@us...> - 2008-06-27 14:54:54
|
Revision: 888
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=888&view=rev
Author: sjp100
Date: 2008-06-27 07:13:33 -0700 (Fri, 27 Jun 2008)
Log Message:
-----------
moved reference to dp to SymbolicInstructionFactory to be consistent with Corina's changes
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicConstraintsGeneral.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-27 00:47:34
|
Revision: 887
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=887&view=rev
Author: pcorina
Date: 2008-06-26 17:47:33 -0700 (Thu, 26 Jun 2008)
Log Message:
-----------
example illustrating symbolic manipulation of the heap
follows lazy initialization algorithm as described in the following paper:
Generalized Symbolic Execution for Model Checking and Testing,
Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser,
in Proceedings of the 9th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS), 2003.
Added Paths:
-----------
trunk/extensions/symbc/examples/symbolicheap/
trunk/extensions/symbc/examples/symbolicheap/MainLazy.java
trunk/extensions/symbc/examples/symbolicheap/Node.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-27 00:12:32
|
Revision: 886
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=886&view=rev
Author: pcorina
Date: 2008-06-26 17:12:31 -0700 (Thu, 26 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-27 00:00:19
|
Revision: 885
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=885&view=rev
Author: pcorina
Date: 2008-06-26 17:00:18 -0700 (Thu, 26 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/Debug.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-26 23:28:57
|
Revision: 884
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=884&view=rev
Author: pcorina
Date: 2008-06-26 16:28:57 -0700 (Thu, 26 Jun 2008)
Log Message:
-----------
added helper methods: makeSymbolic
moved Debug and associated JPF_ class here (it was in test before)
Added Paths:
-----------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/Debug.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-26 23:27:47
|
Revision: 883
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=883&view=rev
Author: pcorina
Date: 2008-06-26 16:27:46 -0700 (Thu, 26 Jun 2008)
Log Message:
-----------
added dp (decision procedure) and code to initialize it
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-26 23:26:48
|
Revision: 882
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=882&view=rev
Author: pcorina
Date: 2008-06-26 16:26:46 -0700 (Thu, 26 Jun 2008)
Log Message:
-----------
removed dp from here
went to SymbolicInstructionFactory
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/BytecodeUtils.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-25 23:18:36
|
Revision: 881
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=881&view=rev
Author: pcmehlitz
Date: 2008-06-25 16:18:30 -0700 (Wed, 25 Jun 2008)
Log Message:
-----------
* the RaceDetector didn't filter field access inside clinits
* StaticFieldInstruction.isSchedulingRelevant() should check if the clinit class and the field declaring class are
the same
The RaceDetector still has daemons in it. Seems it's interfering with the POR sync detection - maybe we should just drop the
thing in favor of the PreciseRaceDetector, which is more efficient and less prone to false positives / false negatives
Modified Paths:
--------------
trunk/examples/DiningPhilosophers/Philosopher.java
trunk/src/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java
trunk/src/gov/nasa/jpf/tools/RaceDetector.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-24 01:00:28
|
Revision: 880
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=880&view=rev
Author: pcmehlitz
Date: 2008-06-23 18:00:27 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
* fixed the broken fix reg. multiple inclusions of the same ThreadInfo into the ThreadList. First, every ThreadInfo
creation should go through ThreadInfo's factory method. Second, there is no easy way around exclusiveness checking
in ThreadInfo.add() - the ThreadInfo cache isn't backtracked, but the ThreadList is. This fixed the DiningPhilosophers
in HeuristicSearch again
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/ThreadList.java
trunk/test/gov/nasa/jpf/mc/TestPartialTraceJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-23 23:29:01
|
Revision: 879
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=879&view=rev
Author: pcmehlitz
Date: 2008-06-23 16:28:59 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
re-iteration on the last two commits:
* transition breaks on Thread.start()/sleep()/yield() should be optional. There now is a "cg.thread.break_all"
to control this, and the default is false
* the ChoicePoint change was using String.isEmpty(), which is not in Java 1.5. Thanks Hank
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ChoicePoint.java
trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-23 22:25:44
|
Revision: 878
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=878&view=rev
Author: pcmehlitz
Date: 2008-06-23 15:25:43 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
* this is a re-iteration of Thread.start(). The thinking was that it would be more understandable if
we have SchedulingPoints when we start a new thread, but that causes state bloat with pure starter
threads that just return after starting their workers. In this case, we get transition breaks
on both the Thread.start() calls and the RETURN insn of the starter, which can be more confusing
than not seeing a reschedule. In any way, the new threads should be RUNNABLE, after the tart call
(if they are not blocked), so any following re-schedule in the starter should see them
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-23 20:57:20
|
Revision: 877
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=877&view=rev
Author: pcorina
Date: 2008-06-23 13:57:18 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicReal.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-23 20:57:09
|
Revision: 876
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=876&view=rev
Author: pcorina
Date: 2008-06-23 13:57:05 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicInteger.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-23 19:23:25
|
Revision: 875
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=875&view=rev
Author: pcmehlitz
Date: 2008-06-23 12:23:22 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
* changed the trace file format so that it only stored the first occurrence of each CG class name, and then refers
to it with #id in subsequent occurrences. Just to make trace files smaller (nobody is going to read them manually anyways)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ChoicePoint.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-23 18:59:29
|
Revision: 874
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=874&view=rev
Author: pcorina
Date: 2008-06-23 11:59:26 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-23 18:55:15
|
Revision: 873
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=873&view=rev
Author: pcmehlitz
Date: 2008-06-23 11:54:17 -0700 (Mon, 23 Jun 2008)
Log Message:
-----------
* ReturnInstruction.set/getReturnAttr() should be public so that it can be used in listeners/overridden bytecode sets
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/bytecode/DRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/RETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-18 07:27:53
|
Revision: 872
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=872&view=rev
Author: pcmehlitz
Date: 2008-06-18 00:27:51 -0700 (Wed, 18 Jun 2008)
Log Message:
-----------
* added \-escapes to Config.getStringArray(), hoping that nobody uses '\' as a dir separator. Also not clear if the escape
chars would get past the java.util.Properties parsing
Modified Paths:
--------------
branches/v5/src/gov/nasa/jpf/Config.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-17 17:09:16
|
Revision: 871
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=871&view=rev
Author: pcmehlitz
Date: 2008-06-17 10:09:06 -0700 (Tue, 17 Jun 2008)
Log Message:
-----------
* changes in Fields/ElementInfo interface, to facilitate type specific ArrayFields, and centralize change
management in ElementInfo. Still needs more changes to accommodate per-field change flags. Fields/FieldInfo is
now more tightly coupled, but ElementInfo doesn't have to know about it
Modified Paths:
--------------
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
branches/v5/examples/issta2006/Linearizer.java
branches/v5/src/gov/nasa/jpf/jvm/Area.java
branches/v5/src/gov/nasa/jpf/jvm/ArrayFields.java
branches/v5/src/gov/nasa/jpf/jvm/ClassInfo.java
branches/v5/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicArea.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfoContainer.java
branches/v5/src/gov/nasa/jpf/jvm/Fields.java
branches/v5/src/gov/nasa/jpf/jvm/FloatFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/Heap.java
branches/v5/src/gov/nasa/jpf/jvm/IntegerFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/LongFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/MJIEnv.java
branches/v5/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/StaticElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/ThreadInfo.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/filter/SimpleFilteringSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sj...@us...> - 2008-06-16 21:34:22
|
Revision: 870
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=870&view=rev
Author: sjp100
Date: 2008-06-16 14:34:12 -0700 (Mon, 16 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/ProblemCVC3.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-16 21:32:35
|
Revision: 869
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=869&view=rev
Author: pcorina
Date: 2008-06-16 14:28:35 -0700 (Mon, 16 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/ProblemCVC3.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-16 21:20:49
|
Revision: 868
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=868&view=rev
Author: pcorina
Date: 2008-06-16 14:20:39 -0700 (Mon, 16 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/ProblemCVC3.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-06-16 21:18:07
|
Revision: 867
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=867&view=rev
Author: pcorina
Date: 2008-06-16 14:18:03 -0700 (Mon, 16 Jun 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/ProblemCVC3.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
