Menu
▾
▴
javapathfinder-devel
|
From: <pcm...@us...> - 2008-01-29 05:19:47
|
Revision: 738
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=738&view=rev
Author: pcmehlitz
Date: 2008-01-28 21:19:44 -0800 (Mon, 28 Jan 2008)
Log Message:
-----------
start to roll in missing contract extensions, but not yet complete
* model space contracts - still needs some polishing, and needs to be aligned with native properties (with which it
shares the same interface in app/). This also requires @Local to be implemeted, to provide additional safeguards
against contract side effects. It's debatable if the model should be "just call arbitrary user code" or "only
allow very restricted user code" to avoid side effects on the state space. For now, we go with the second one, otherwise
we have to introduce a synthetic wrapper around contracted method calls. The reason is that I see this as a last
measure anyways, and expect the majority of contract types to be built-in or native side
@Local could be a very useful property on its own, think I do this next as a complement to @Const (which also needs
to be integrated into ContractVerifier)
* had to refactor Contract for this, pulling the generic Satisfies to toplevel
* added very minimalistic support for DateFormat parsing
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractContext.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/Local.java
trunk/app/gov/nasa/jpf/Predicate.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DateFormat.java
trunk/src/gov/nasa/jpf/test/Satisfies.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-30 02:10:16
|
Revision: 739
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=739&view=rev
Author: pcmehlitz
Date: 2008-01-29 18:10:12 -0800 (Tue, 29 Jan 2008)
Log Message:
-----------
* bug in propagation of double-word local slots (the "?" fillers screwed up the slot offset calculation when
retrieving the lvar)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-01 07:21:24
|
Revision: 740
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=740&view=rev
Author: pcmehlitz
Date: 2008-01-31 23:21:22 -0800 (Thu, 31 Jan 2008)
Log Message:
-----------
* some more java.util.Random methods (but CGs for the enumerate_random mode still missing)
* seamless integration of native and model properties. Maybe it's a bit too seamless, since
both implement the same interface (Predicate), but in all likeliness differ substantially in
implementation (the 'Object' parameters are different). Worked around that by adding a type tag
interface 'NativePredicate' but that's not very type safe.
The Satisfies predicate lookup had to be changed in order to avoid confusion when executing JPF
with the native predicates in the JPF classpath (e.g. when running from within Eclipse)
* added a native example predicate 'IsMonotonicDecreasing', which shows why we might want native
predicates (carries state we don't want in the model). Isn't checked for proper backtracking behavior yet
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/src/gov/nasa/jpf/test/ContractContext.java
trunk/src/gov/nasa/jpf/test/Satisfies.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/ExecBounds.java
trunk/app/gov/nasa/jpf/NoAlloc.java
trunk/app/gov/nasa/jpf/NoBlock.java
trunk/src/gov/nasa/jpf/test/NativePredicate.java
trunk/src/gov/nasa/jpf/test/predicate/
trunk/src/gov/nasa/jpf/test/predicate/IsMonotonicDecreasing.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/test/Predicate.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-01 18:45:16
|
Revision: 741
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=741&view=rev
Author: pcmehlitz
Date: 2008-02-01 10:45:06 -0800 (Fri, 01 Feb 2008)
Log Message:
-----------
* added an Verify.setProperties(String...p) to programmatically set JPF properties at runtime from within the
model
* using this, extended the TestContracts example to show how to implement NativePredicates that are backtracking aware
- nice demo!
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-05 23:04:22
|
Revision: 742
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=742&view=rev
Author: pcmehlitz
Date: 2008-02-05 15:04:14 -0800 (Tue, 05 Feb 2008)
Log Message:
-----------
* some left over doc updates
* empty event scripts caused parse exception, which they shouldn't
* revisited the unbounded REPEATs, but this is not functional yet. Needs to add a pseudo CG in EventGeneratorFactory,
which is used only to position in the CG queue. This would be some sort of a script insn, which we hadn't so far. Just
used simple unrolling to keep the backtracking simple, but of course that doesn't work with unbounded REPEATs
Modified Paths:
--------------
trunk/doc/JPF_files/JPF-mod.css
trunk/doc/home.html
trunk/doc/news.html
trunk/extensions/symbc/doc/index.html
trunk/src/gov/nasa/jpf/util/script/ESParser.java
Added Paths:
-----------
trunk/extensions/statechart/examples/Repeat.es
trunk/extensions/statechart/examples/Repeater.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-06 22:13:37
|
Revision: 743
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=743&view=rev
Author: pcmehlitz
Date: 2008-02-06 14:13:19 -0800 (Wed, 06 Feb 2008)
Log Message:
-----------
* added partial wildcard ANYs to scripts, so you can do a
ANY { foo, bar, *baz }
which still causes alphabet expansion (to get all trigger methods of all active states via reflection), but then filters
by matching all found trigger names against the ANY patterns. This is actually more straight than the previous
ANY { * }, which is really just a special case
* added some 'hasAnyPattern' optimization to StringSetMatcher - no need to burn a lot of cycles on regex matching
if we know there is a "matches anything" pattern
* first stab on unbounded REPEATs, but there are subtle search termination issues remaining. This introduces
'instructions' (pseudo CGs) into the EventGeneratorFactory queue, which works Ok but should be refactored so that
we don't have to call the Jump a ChoiceGenerator. What doesn't work so well is that it creates infinite loops
if we never run out of active states (e.g. if triggers do not fire a transition). This is because with unconditional
Jumps we never run out of fresh CGs (the next CG is always reset in EventGeneratorFactory.getNextChoiceGenerator()). The
JVM nicely recognizes if it has visited a program state, but of course always goes on if the next CG says it still
has choices (because it was reset). So we need to make the Jump conditional, i.e. give it it's own state.
Once this is done, it should be used as the sole mechanism for REPEATs, and we should ditch the unrolling
Modified Paths:
--------------
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/examples/Repeater.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventFromSet.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGenerator.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventSingleChoice.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/util/StringSetMatcher.java
trunk/src/gov/nasa/jpf/util/script/ESParser.java
trunk/src/gov/nasa/jpf/util/script/EventGeneratorFactory.java
Added Paths:
-----------
trunk/extensions/statechart/examples/Wildcards.es
trunk/extensions/statechart/examples/Wildcards.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-08 02:07:14
|
Revision: 744
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=744&view=rev
Author: pcmehlitz
Date: 2008-02-07 18:07:07 -0800 (Thu, 07 Feb 2008)
Log Message:
-----------
* added a more intuitive State.terminate(), which is synonym to State.setEndState(<masterState>), to terminate
the whole execution. Be aware this still processes all exitActions of the issuing state up to the masterState
* fixed a bug in StateMachine.step(), which caused the masterState to be erroneously added to the nextActives set
in case somebody globally terminates
* changed State.getName() to return the typeName if there is no fieldName, which is more readable if somebody
does things with the masterState (which doesn't have a fieldName)
Modified Paths:
--------------
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/JPF_gov_nasa_jpf_sc_StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/examples/Ortho1.java
trunk/extensions/statechart/examples/Repeater.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
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.
|
|
From: <pcm...@us...> - 2008-02-15 06:01:09
|
Revision: 745
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=745&view=rev
Author: pcmehlitz
Date: 2008-02-14 22:01:07 -0800 (Thu, 14 Feb 2008)
Log Message:
-----------
* added an abstract factory to create Fields instances, which is a precursor for a customized object storage
model. We don't have that yet, but this also enables logging *all* field manipulations (incl. attributes), which
also comes in handy for the upcoming "undo" mode. What is not so nice is that we have to pass in a usually
not used reference to the ElementInfo holding the fields, which in turn required changing the default field init
(from consts). This now requires explicit initialization calls from Dynamic/StaticArea, whereas before it was
just part of the Fields creation.
With this, UntrackedManager references should be removed from the default Fields impl
The FieldsFactory class can be set with the 'vm.fields_factory.class' property, which was added to default.properties
Modified Paths:
--------------
trunk/.classpath
trunk/default.properties
trunk/examples/jpfESAS/launch/CV-assumption-1.launch
trunk/examples/launch/conc-2-RA_da.launch
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/DynamicElementInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicFields.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/FloatFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/IntegerFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/LongFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/StaticArea.java
trunk/src/gov/nasa/jpf/jvm/StaticElementInfo.java
trunk/src/gov/nasa/jpf/jvm/StaticFields.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedManager.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/jvm/DefaultFieldsFactory.java
trunk/src/gov/nasa/jpf/jvm/FieldsFactory.java
Removed Paths:
-------------
trunk/examples/jpfESAS/launch/CEV-las-defect.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-21 05:33:47
|
Revision: 754
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=754&view=rev
Author: pcmehlitz
Date: 2008-02-20 21:33:41 -0800 (Wed, 20 Feb 2008)
Log Message:
-----------
* don't queue sendEvent() entries when running scriptless, which would not only be pointless but also
screw state matching.
* add an MJIEnv.setReturnAttr(attr), so that we can set operand attrs from within native peer methods
(on return values).
Modified Paths:
--------------
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/JPF_gov_nasa_jpf_sc_StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/NativePeer.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-22 00:38:14
|
Revision: 757
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=757&view=rev
Author: pcmehlitz
Date: 2008-02-21 16:38:12 -0800 (Thu, 21 Feb 2008)
Log Message:
-----------
* added a 'vm.peer_packages' property which can be used to specify an ordered list of packages we try to
locate native peer classes. This is required to override native peer implementations from extension. The
alternative would have been to try all packages in the classpath, i.e. control the lookup with the
classpath order, but that would be VERY inefficient since there are gazillions of packages in the usual
classpath (the jars!)
Modified Paths:
--------------
trunk/default.properties
trunk/extensions/statechart/examples/CompletionSend.es
trunk/extensions/statechart/examples/CompletionSend.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/NativePeer.java
Added Paths:
-----------
trunk/examples/jpfESAS/launch/CEV-las-defect.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-22 04:25:37
|
Revision: 761
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=761&view=rev
Author: pcmehlitz
Date: 2008-02-21 20:25:35 -0800 (Thu, 21 Feb 2008)
Log Message:
-----------
* added an MJIEnv.getOperandAttrs() so that we can get and set operand attrs from within native methods.
This came up with the java.lang.Math native peer for symbolic exec, but will be helpful for the
numeric extension too
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestAttrs.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-02-22 23:26:10
|
Revision: 765
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=765&view=rev
Author: pcorina
Date: 2008-02-22 15:26:09 -0800 (Fri, 22 Feb 2008)
Log Message:
-----------
added suport for Math lib functions (sin, cos, and pow)
should be run with option;
+vm.peer_packages=gov.nasa.jpf.symbc:gov.nasa.jpf.jvm
comitted an example ExSymExePrecondAndMath that shows
handling of precond and Math functions.
Modified Paths:
--------------
trunk/.classpath
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExe.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeDDIV.java
Added Paths:
-----------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_MathOld.java
trunk/extensions/symbc/env/
trunk/extensions/symbc/env/jvm/
trunk/extensions/symbc/env/jvm/gov/
trunk/extensions/symbc/env/jvm/gov/nasa/
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_Math.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExePrecondAndMath.java
Removed 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: <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: <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: <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: <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: <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: <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: <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-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-26 20:26:37
|
Revision: 794
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=794&view=rev
Author: pcmehlitz
Date: 2008-03-26 13:26:34 -0700 (Wed, 26 Mar 2008)
Log Message:
-----------
* added pattern matching for receiver constraints in event scripts. This is never going to end <SIGH>.
We have to push the filtering down into the alphabet inspection, since we have to add the receiver to the list of candidates
in case there is a receiverConstraint. Otherwise we might just add the event id, even though there is a constraint
in the script, and then get surprised during executeTrigger() because there is another active state that has this
trigger method. If there already is an rc-event with the same event name in the set, add the active state field name
to the rc. If there is the same event name but no rc, then it's pointless to add a constraint
this also unveiled a little bug with a forgotten matcher for SCEventSingleChoice
Modified Paths:
--------------
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/SCEventFromSet.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGenerator.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventSingleChoice.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/util/script/ScriptEnvironment.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-04-03 21:29:47
|
Revision: 798
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=798&view=rev
Author: pcmehlitz
Date: 2008-04-03 14:29:45 -0700 (Thu, 03 Apr 2008)
Log Message:
-----------
* small patch for Verify.getInt(), avoiding CG creation if the boundaries are identical - thanks to Gliga
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/util/DynamicObjectArray.java
trunk/test/gov/nasa/jpf/mc/TestUntrackedField.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X