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: <ubn...@us...> - 2008-03-26 18:00:30
|
Revision: 793
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=793&view=rev
Author: ubnepvpb
Date: 2008-03-26 10:59:32 -0700 (Wed, 26 Mar 2008)
Log Message:
-----------
Move INVOKExxx.execute() to BytecodeUtils.execute() so we don't have the same code in lots of different places.
Add some more self-checking test cases.
Fix LineNumberListener so it does not print line numbers for code in the packages "java.what.ever".
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/BytecodeUtils.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESPECIAL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESTATIC.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKEVIRTUAL.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/LineNumberListener.java
Added Paths:
-----------
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestBooleanStatic1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDoubleStatic1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestFloatStatic1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestIntStatic1.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: John P. <jp...@go...> - 2008-03-26 08:02:06
|
Hi Mateusz, (Sorry for the delayed reply.) I've cc'ed the jpf-devel list and Peter Mehlitz. Excellent - this could be a very helpful project and you look like a good match for it. I think the way to do this would be to start with some sample programs from Doug Lea's book (or other sources) and first see if they even run on JPF. There could be problems with native methods that JPF doesn't support. Supporting those native methods via the JMI would be a good start. Then, you would look for inefficiencies in terms of the number of states that JPF is storing or poor time performance to identify places were a JMI implementation of a util.concurrent method or class would make a significant different in how JPF ran on the program. I signed up as the mentor for this because I think it's important - I'm not actually very familiar with the util.concurrent library. But I'm guessing we might want to pick one or two of the synchronization primitives to support as the main goal, and expand from there is things go well. It's usually hard to guess ahead of time exactly where JPF might have problems with a library - but Peter might have a good guess. In terms of your application, I think with your background knowledge, you are half-way there. If you have ideas on specific constructs that you would like to focus on first and an locate example code that would be great. If we could track down a real program that uses java.util.concurrentthat you could use as a test, that would a be fantastic proposal. John On Sun, Mar 23, 2008 at 6:23 PM, Mateusz Ujma <mat...@gm...> wrote: > Hi, > > My name is Mateusz Ujma and I'm really interested in project #4. > I've read > http://javapathfinder.sourceforge.net/The_Model_Java_Interface.html > so I've really rough idea how it can be done. Could you give me some > more information about this project. What are the main steps, what > websites I should visit to write good proposal > etc ? If project #4 is considered by many students I would appreciate > that information so I will be able to focus on some less overcrowded > ideas. > > Few words about myself: > > Currently I'm on fourth year of Computer Science MS.c studies at > Cracow University of Technology. I was part of Motorola scholarship > that covered topics > about distributed and real time systems(i.e. Petri nets). Last year I > took part in GSoC with SilverStripe organization(successfully). After > GSoC I was able to > focus my university project on SilverStripe so I remained active > developer. Since october I'm working as > R&D consultant at Onet.pl(biggest polish portal) developing Java > applications for embedded systems(STB). Considering concurrency in Java > I've used > java.utils.concurrent and it backports to java 1.3. I'm also after > extensive reading of Java Concurrency in Practice by Brian Goetz, Doug > Lea. > > Best regards > > Mateusz Ujma > |
|
From: John P. <jp...@go...> - 2008-03-26 07:02:07
|
I just posted this list as the team contact on Google Summer of Code! |
|
From: <pcm...@us...> - 2008-03-24 22:08:49
|
Revision: 792
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=792&view=rev
Author: pcmehlitz
Date: 2008-03-24 15:08:47 -0700 (Mon, 24 Mar 2008)
Log Message:
-----------
* removed the direct 'hasChanged' references from the State Restorers/Serializers. The important thing is that
they shouldn't rely on a specific Area implementation (which is just about to change - this is cleaning up the
playground). But BitSet actually got quite efficient, and it's worth it to change the iteration to
BitSet.nextSetBit() (slight performance gain in itself)
Modified Paths:
--------------
trunk/default.properties
trunk/extensions/undo/src/gov/nasa/jpf/jvm/UndoRestorer.java
trunk/src/gov/nasa/jpf/jvm/Area.java
trunk/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
trunk/src/gov/nasa/jpf/jvm/CollapsingSerializer.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-21 16:33:09
|
Revision: 791
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=791&view=rev
Author: pcmehlitz
Date: 2008-03-21 09:33:06 -0700 (Fri, 21 Mar 2008)
Log Message:
-----------
* inconsistency of binary location for 'app' sources between .classpath and build.xml. Should go in it's own
build/app dir (this stuff is supposed to be used by applications that otherwise don't want JPF in their
classpath) - thanks to Steve
Modified Paths:
--------------
trunk/.classpath
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-21 16:16:06
|
Revision: 790
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=790&view=rev
Author: pcmehlitz
Date: 2008-03-21 09:16:03 -0700 (Fri, 21 Mar 2008)
Log Message:
-----------
* bug in growing locals in DirectCallStackFrame - thanks to Gliga
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/DirectCallStackFrame.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-21 16:11:53
|
Revision: 789
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=789&view=rev
Author: pcmehlitz
Date: 2008-03-21 09:11:51 -0700 (Fri, 21 Mar 2008)
Log Message:
-----------
* some doc corrections from Darko Marinov
Modified Paths:
--------------
trunk/doc/Model_Checking_vs_Testing.html
trunk/doc/RegressionTests.html
trunk/doc/Running_JPF.html
trunk/doc/The_State_of_Affairs.html
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedField.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-21 16:09:37
|
Revision: 788
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=788&view=rev
Author: pcmehlitz
Date: 2008-03-21 09:09:33 -0700 (Fri, 21 Mar 2008)
Log Message:
-----------
* added 'undo' extension from Tihomir Gvero. This stores/reverts field writes instead of storing data snapshots, and can be
significantly more efficient when modifying small parts on large data structures (single elements in large arrays)
Modified Paths:
--------------
trunk/.classpath
trunk/doc/extensions.html
trunk/src/gov/nasa/jpf/jvm/Area.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/SimpleFilteringSerializer.java
trunk/src/gov/nasa/jpf/tools/HeapTracker.java
Added Paths:
-----------
trunk/extensions/undo/
trunk/extensions/undo/build.xml
trunk/extensions/undo/doc/
trunk/extensions/undo/doc/index.html
trunk/extensions/undo/src/
trunk/extensions/undo/src/gov/
trunk/extensions/undo/src/gov/nasa/
trunk/extensions/undo/src/gov/nasa/jpf/
trunk/extensions/undo/src/gov/nasa/jpf/UndoListener.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/
trunk/extensions/undo/src/gov/nasa/jpf/jvm/KState.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/UndoDynamicFactory.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/UndoFactory.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/UndoRestorer.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/UndoStaticFactory.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoArea.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoArrayFields.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoBacktracker.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoCloneableFields.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoDynamicFields.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoFieldsFactory.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoObject.java
trunk/extensions/undo/src/gov/nasa/jpf/jvm/undo/UndoStaticFields.java
trunk/extensions/undo/test/
trunk/extensions/undo/test/gov/
trunk/extensions/undo/test/gov/nasa/
trunk/extensions/undo/test/gov/nasa/jpf/
trunk/extensions/undo/test/gov/nasa/jpf/jvm/
trunk/extensions/undo/test/gov/nasa/jpf/jvm/undo/
trunk/extensions/undo/test/gov/nasa/jpf/jvm/undo/TestUndo.java
trunk/extensions/undo/test/gov/nasa/jpf/jvm/undo/TestUndoJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-03-21 01:06:42
|
Revision: 787
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=787&view=rev
Author: pcorina
Date: 2008-03-20 18:06:39 -0700 (Thu, 20 Mar 2008)
Log Message:
-----------
added first info about decision procedures
Added Paths:
-----------
trunk/extensions/symbc/ReadmeMultipleDecisionProcedures
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-03-19 23:59:11
|
Revision: 786
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=786&view=rev
Author: pcorina
Date: 2008-03-19 16:59:08 -0700 (Wed, 19 Mar 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/PCChoiceGenerator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-19 19:35:35
|
Revision: 785
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=785&view=rev
Author: pcmehlitz
Date: 2008-03-19 12:35:32 -0700 (Wed, 19 Mar 2008)
Log Message:
-----------
* finally made the Dynamic/StaticArea classes configurable, so that heap representations can be changed.
* with that, moved all the @UntrackedField functionality into its own package. Downside is that it requires
a lot more configuration to use it, but it was proliferating the core more than what seemed to be
justifiable by potential uses. The refactoring is Ok for most parts, only the Fields duplication sucks
(the old modified-baseclass problem).
Maybe we move this into its own extension at some point (better for the test and the app-relevant annotation)
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/jvm/Area.java
trunk/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/KernelState.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedField.java
trunk/test/gov/nasa/jpf/mc/TestUntrackedField.java
trunk/test/gov/nasa/jpf/mc/TestUntrackedFieldJPF.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedArrayFields.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedCollapsingRestorer.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedDynamicArea.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedDynamicFields.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedFields.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedFieldsFactory.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedStaticArea.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedStaticFields.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-03-19 00:23:03
|
Revision: 784
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=784&view=rev
Author: pcorina
Date: 2008-03-18 17:23:00 -0700 (Tue, 18 Mar 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/bytecode/SwitchInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-03-19 00:14:07
|
Revision: 783
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=783&view=rev
Author: pcorina
Date: 2008-03-18 17:14:05 -0700 (Tue, 18 Mar 2008)
Log Message:
-----------
added support for switch statements.
Warning: the NE operator from choco is really broken, so switch may not work properly.
I will try to update to the new version of choco or we should switch to another, more reliable constraint solver (maybe with Suzette we should add CVC3).
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/MinMax.java
Added Paths:
-----------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/LOOKUPSWITCH.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/SwitchInstruction.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/TABLESWITCH.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-18 05:39:10
|
Revision: 782
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=782&view=rev
Author: pcmehlitz
Date: 2008-03-17 22:39:08 -0700 (Mon, 17 Mar 2008)
Log Message:
-----------
* little POR optimization that can have a significant impact: "synchronized (myfield){..}" is usually compiled
into some "getfield; dup; [astore;] monitorenter" pattern. If we see this pattern (fairly inexpensive test),
we skip the transition break for the getfield and rely on the subsequent monitorenter. Could be more
sophisticated ("Object o = myfield; synchronized(o){..}
Modified Paths:
--------------
trunk/doc/On-the-fly_Partial_Order_Reduction.html
trunk/doc/Running_JPF.html
trunk/src/gov/nasa/jpf/jvm/SingleFieldLockInfo.java
trunk/src/gov/nasa/jpf/jvm/StatisticFieldLockInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FieldInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java
trunk/src/gov/nasa/jpf/jvm/bytecode/NEW.java
trunk/src/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-03-13 21:40:41
|
Revision: 781
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=781&view=rev
Author: pcorina
Date: 2008-03-13 14:40:38 -0700 (Thu, 13 Mar 2008)
Log Message:
-----------
changed from mi.execute to super.execute (thanks hank)
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESTATIC.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-03-13 21:40:10
|
Revision: 780
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=780&view=rev
Author: pcorina
Date: 2008-03-13 14:40:07 -0700 (Thu, 13 Mar 2008)
Log Message:
-----------
changed from mi.execte to super.execute (thanks hank)
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESPECIAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-13 02:34:27
|
Revision: 779
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=779&view=rev
Author: pcmehlitz
Date: 2008-03-12 19:34:17 -0700 (Wed, 12 Mar 2008)
Log Message:
-----------
* bug in executeTrigger() methods of both StateMachines - method matching has to be done recursively on
both enclosing and inheritance hierarchy, while receiver matching should only be performed on the
concrete (mdc) state. This came up with an enclosing class that wasn't a direct State subclass (KC TM_1 example)
Modified Paths:
--------------
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-03-12 19:16:04
|
Revision: 778
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=778&view=rev
Author: pcorina
Date: 2008-03-12 12:15:58 -0700 (Wed, 12 Mar 2008)
Log Message:
-----------
Fixed problem with choices comming from super in INVOKE classes.
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESPECIAL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESTATIC.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-11 06:16:59
|
Revision: 777
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=777&view=rev
Author: pcmehlitz
Date: 2008-03-10 23:16:55 -0700 (Mon, 10 Mar 2008)
Log Message:
-----------
* changed the implementation of the active/nextActive sets from state tracked StateMachine State[] fields to
non-state tracked linked lists by adding a State.next field (how often can you say 'State' in one sentence?)
The idea was that this would save state storage memory in case of large active sets (the things didn't shrink), but it
didn't do its magic on Plexil. Except of that it got a lot faster - so it's happily committed anyways
The state matching now is done on the added 'isActive' field in State. Note that we can't rely on StateMachine.activeStates
traversal during a step, since there is a constant re-queuing (between active and nextActive) going on (i.e. the
'next' field changes its meaning)
* added a +sc.show_machine option that can be used to print the state hierarchy before we start to execute
* added search constraint reporting to the Reporter/Publisher so that we don't have magic terminations
w/o apparent reason anymore. I was positively surprised that at least OS/X and Linux now handle
OutOfMemory conditions gracefully
Modified Paths:
--------------
trunk/default.properties
trunk/examples/jpfESAS/launch/CEV-las-defect.launch
trunk/examples/jpfESAS/launch/CEV-tli-sim.launch
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SCInspector.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/ListenerAdapter.java
trunk/src/gov/nasa/jpf/PropertyListenerAdapter.java
trunk/src/gov/nasa/jpf/jvm/AbstractSerializer.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/SimpleFilteringSerializer.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/Publisher.java
trunk/src/gov/nasa/jpf/report/PublisherExtension.java
trunk/src/gov/nasa/jpf/report/Reporter.java
trunk/src/gov/nasa/jpf/search/DFSearch.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/util/script/ScriptEnvironment.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ubn...@us...> - 2008-03-07 01:24:35
|
Revision: 776
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=776&view=rev
Author: ubnepvpb
Date: 2008-03-06 17:24:21 -0800 (Thu, 06 Mar 2008)
Log Message:
-----------
Make symbc.INVOKEVIRTUAL and symbc.INVOKESPECIAL more alike.
Add some self-checking test cases for INVOKEVIRTUAL.
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESPECIAL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKEVIRTUAL.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDoubleVirtual1.java
Added Paths:
-----------
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestBooleanVirtual1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestFloatVirtual1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestIntVirtual1.java
Property Changed:
----------------
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-03-06 07:15:59
|
Revision: 775
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=775&view=rev
Author: pcmehlitz
Date: 2008-03-05 23:15:53 -0800 (Wed, 05 Mar 2008)
Log Message:
-----------
* created generic StateExtensionListener/Client to better support backtrackable state extensions like script environment
states etc
* added Iterators to the ScriptElementContainer hierarchy, which also handles the loops in Repetition
* created a SequenceInterpreter to enable control flow in scripts (e.g. real loops)
* used all that to create a ScriptEnvironment that replaces the old and rather flawed EventGeneratorFactory. This
keeps track of active sequences and associated interpreters. A rather expensive mechanism, but conceptually cleaner
than the old EventGeneratorFactory that became a mess with sequence composition and loops
* used this to move the statechart extension over to ScriptEnvironment
* modified the NativeStateMachine to use event polymorphism instead of the braindead updateList / EventSource
to remove/pool PendingEvents when they are processed. We can do this since we already have the SCEvent factory method
in NativeSateMachine
* now keep track of re-entered states, even though the jury is still out if script sections should be restarted
by self transitions
* fixed missing sync CGs in INVOKESPECIAL (refactored into InvokeInstruction)
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEventQueue.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
trunk/src/gov/nasa/jpf/util/Misc.java
trunk/src/gov/nasa/jpf/util/script/Alternative.java
trunk/src/gov/nasa/jpf/util/script/ESParser.java
trunk/src/gov/nasa/jpf/util/script/Event.java
trunk/src/gov/nasa/jpf/util/script/EventGeneratorFactory.java
trunk/src/gov/nasa/jpf/util/script/Repetition.java
trunk/src/gov/nasa/jpf/util/script/Script.java
trunk/src/gov/nasa/jpf/util/script/ScriptElement.java
trunk/src/gov/nasa/jpf/util/script/ScriptElementContainer.java
trunk/src/gov/nasa/jpf/util/script/Section.java
Added Paths:
-----------
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCScriptEnvironment.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SentSCEvent.java
trunk/src/gov/nasa/jpf/StateExtension.java
trunk/src/gov/nasa/jpf/util/StateExtensionClient.java
trunk/src/gov/nasa/jpf/util/StateExtensionListener.java
trunk/src/gov/nasa/jpf/util/script/ScriptEnvironment.java
trunk/src/gov/nasa/jpf/util/script/SequenceInterpreter.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ubn...@us...> - 2008-03-06 01:09:08
|
Revision: 774
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=774&view=rev
Author: ubnepvpb
Date: 2008-03-05 17:09:04 -0800 (Wed, 05 Mar 2008)
Log Message:
-----------
Some cleanup in the INVOKExxx instructions.
Some new tests.
Fix SymbolicInstructionFactory: it was not using the IAND bytecode from symbc.
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/BytecodeUtils.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESPECIAL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESTATIC.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKEVIRTUAL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicInteger.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDoubleSpecial1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestFloatSpecial1.java
Added Paths:
-----------
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestBooleanSpecial1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestIntSpecial1.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ar...@us...> - 2008-03-01 00:58:24
|
Revision: 773
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=773&view=rev
Author: artimid
Date: 2008-02-29 16:58:13 -0800 (Fri, 29 Feb 2008)
Log Message:
-----------
Temporary commit that fixed the problem of events being removed from queue. more detailed commit message next week. lots of debugging printouts still there. Will be fixed.
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEventQueue.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ar...@us...> - 2008-02-29 00:43:18
|
Revision: 772
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=772&view=rev
Author: artimid
Date: 2008-02-28 16:43:16 -0800 (Thu, 28 Feb 2008)
Log Message:
-----------
Removed some debugging prints
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEventQueue.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-29 00:14:17
|
Revision: 771
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=771&view=rev
Author: pcmehlitz
Date: 2008-02-28 16:14:12 -0800 (Thu, 28 Feb 2008)
Log Message:
-----------
* bad EventGenerator loop fix - we have to reset CGs before re-entering the loop, not per default. However, that leaves
model loops to be broken because they get prematurely state matched.
Anyways, the EventGeneratorFactory mechanism is broken, since control operations (like loops) were not in the original
script semantics. Hence it will be replaced by an AST-based interpreter soon, which is where we really fix things
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/util/script/EventGeneratorFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
