Menu
▾
▴
javapathfinder-devel
|
From: <pcm...@us...> - 2007-02-07 23:31:55
|
Revision: 235
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=235&view=rev
Author: pcmehlitz
Date: 2007-02-07 15:31:53 -0800 (Wed, 07 Feb 2007)
Log Message:
-----------
* context specific TextPanel extensions for the Inspector
* used that in the SCInspector to log to a dedicated logConsole, and to
load the sources of the statechart class
* had to slightly extend the LogManager for this so that the output
target for our LogHandler can be set explicitly (good we only have one)
* minor corrections & extensions for the Listener docu, due to popular request
Modified Paths:
--------------
trunk/doc/Search-_and_VMListeners.html
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SCInspector.java
trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/util/Inspector.java
trunk/src/gov/nasa/jpf/util/LogHandler.java
trunk/src/gov/nasa/jpf/util/LogManager.java
trunk/src/gov/nasa/jpf/util/Source.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-08 00:07:31
|
Revision: 236
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=236&view=rev
Author: pcmehlitz
Date: 2007-02-07 16:07:29 -0800 (Wed, 07 Feb 2007)
Log Message:
-----------
* removed the annoying snapshot printout in ConsolePublisher if the program is back
in initial state. No point in printing this out
* added a dummy java.lang.Runtime native peer, just to avoid
UnsatisfiedLinkErrors
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/Reporter.java
Added Paths:
-----------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Runtime.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-08 06:57:46
|
Revision: 237
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=237&view=rev
Author: pcmehlitz
Date: 2007-02-07 22:57:45 -0800 (Wed, 07 Feb 2007)
Log Message:
-----------
* cleanup of default.properties : search.print_errors and search.print_path are gone
* changed initialization of SystemState.recordSteps, to be delayed until we have
the reporter set up (which is a system listener). It's set if any of the
configured Publishers has a 'trace' topic
* extended Reporter and Publisher interface accordingly
* removed corresponding fragments from Error - it has no saying in the
report generation anymore
* initial stab at search.mutiple_errors, but it's not functional yet
Modified Paths:
--------------
trunk/default.properties
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Runtime.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/src/gov/nasa/jpf/Error.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/SystemState.java
trunk/src/gov/nasa/jpf/report/Publisher.java
trunk/src/gov/nasa/jpf/report/Reporter.java
trunk/src/gov/nasa/jpf/search/Search.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: Peter C. M. <pcm...@em...> - 2007-02-12 18:29:26
|
Sergey, just add "trace" to the list of "property_violation" publisher topics, as in jpf.report.console.property_violation=error:trace:snapshot There are a bunch of "show_X" options that can be used to control the amount of info that goes into a trace. The "toXML" is pretty much superseded by the XML publisher (but that one isn't yet updated to the new publishing scheme). I will add some docu about the reporting system shortly. -- Peter On Feb 12, 2007, at 9:36 AM, Sergey Kulikov wrote: > Hi, > > I have a question, there is no more 'path to error' output, and I > also saw in the code that the 'toXML' feature was commented out > (which printed the same path to error in an xml file). > > Just wondering if there's going to be another way of reporting the > path to error? > > thanks > sergey |
|
From: Sergey K. <se...@cs...> - 2007-02-12 20:45:59
|
Hi Peter,
the option
> jpf.report.console.property_violation=error:trace:snapshot
is set on by default in my default.properties file, however only the last
transition is printed out, not the complete trace. Is there any other
option that I need to add to turn the trace on, or is the tracing not
completely implemented as yet.
thanks
sergey
On Mon, 12 Feb 2007, Peter C. Mehlitz wrote:
> Sergey,
>
> just add "trace" to the list of "property_violation" publisher topics, as in
>
> jpf.report.console.property_violation=error:trace:snapshot
>
> There are a bunch of "show_X" options that can be used to control the amount
> of info that goes into a trace. The "toXML" is pretty much superseded by the
> XML publisher (but that one isn't yet updated to the new publishing scheme).
>
> I will add some docu about the reporting system shortly.
>
> -- Peter
>
> On Feb 12, 2007, at 9:36 AM, Sergey Kulikov wrote:
>> Hi,
>>
>> I have a question, there is no more 'path to error' output, and I also saw
>> in the code that the 'toXML' feature was commented out (which printed the
>> same path to error in an xml file).
>>
>> Just wondering if there's going to be another way of reporting the path to
>> error?
>>
>> thanks
>> sergey
>
|
|
From: <pcm...@us...> - 2007-02-08 07:45:00
|
Revision: 238
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=238&view=rev
Author: pcmehlitz
Date: 2007-02-07 23:44:56 -0800 (Wed, 07 Feb 2007)
Log Message:
-----------
* second stab on search.multiple_errors. Kind of works, but two things missing:
(a) the violated Property needs to reset (added to the interface), and I'm
not sure if that's working for all properties (like RaceDetector)
(b) the trace report has to run over the errors, not query the path
out of the VM. Actually, we have to clone paths when we go on, which
is BAD for huge apps with long traces
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/src/gov/nasa/jpf/Error.java
trunk/src/gov/nasa/jpf/GenericProperty.java
trunk/src/gov/nasa/jpf/Property.java
trunk/src/gov/nasa/jpf/jvm/NoUncaughtExceptionsProperty.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/tools/PreciseRaceDetector.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...> - 2007-02-09 20:00:36
|
Revision: 242
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=242&view=rev
Author: pcmehlitz
Date: 2007-02-09 12:00:34 -0800 (Fri, 09 Feb 2007)
Log Message:
-----------
* report system overhaul to support search.multiple_errors. this mainly involves restructuring the
publishers to print out property violations on the go. It just doesn't make sense to not keep
error description, snaphot, trace and path output sections for each property violation together.
As a consequence, publisher topic lists are now broken down into phases: start, transition,
property violation, finished. The property files have to be updated accordingly
(e.g. jpf.report.console.property_violation=error:snapshot:trace)
Since the traces/snapshots are reported on-the-fly, we theoretically don't have to
deep copy paths and snapshots anymore. It would be still required if somebody wants
to process this in searchFinished(), but it can be terribly expensive, so I probably
have to turn that into an option
I haven't updated the XMLPublisher yet, so that thing is currently broken
* vm.path_output is gone - it is synonym to having an "output" topic in any of the
configured publishers (same as the old search.print_errors - if no one publishes "trace"
we don't need to store it)
* based on the Fujitsu experience, I have extended the "statistics" topic data collection
so that we can get useful insights w/o a subsequent SearchMonitor run
Modified Paths:
--------------
trunk/default.properties
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.java
trunk/src/gov/nasa/jpf/Error.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/JVM.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/report/Statistics.java
trunk/src/gov/nasa/jpf/report/XMLPublisher.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/tools/ChoiceTracker.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-11 02:00:56
|
Revision: 244
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=244&view=rev
Author: pcmehlitz
Date: 2007-02-10 18:00:48 -0800 (Sat, 10 Feb 2007)
Log Message:
-----------
* used the BreakGenerator in the AssertionProperty to avoid state explosion when all
we want is a simple transition break. Added a ThreadInfo.breakTransition() to do that
* turned the statechart Coverage tool into a Property. This is an example of a property
that collects data during execution (search/vm listener), but is only evaluated when the
search finishes. Still a bit clumsy, but shows how to do some sort of liveness
Modified Paths:
--------------
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/search/SearchListenerMulticaster.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/tools/AssertionProperty.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-11 21:20:07
|
Revision: 245
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=245&view=rev
Author: pcmehlitz
Date: 2007-02-11 13:20:04 -0800 (Sun, 11 Feb 2007)
Log Message:
-----------
* changed exception handling in state machine execution - it's now completely
delegated to the machine, so that we don't run the danger that we
have "catch(Throwable)" handlers that could shoot the model checker in the
foot. Some more indirection, but at least state method execution is now handled
consistently, and the SimStateMachine doesn't go on after hitting an
exception in such a method
* changed the ChoiceTracker a bit so that it doesn't report CGs on the
stack that are done (carry over CGs in state machine execution)
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/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/jvm/ChoiceGenerator.java
trunk/src/gov/nasa/jpf/tools/ChoiceTracker.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcd...@us...> - 2007-02-12 20:24:02
|
Revision: 246
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=246&view=rev
Author: pcdillinger
Date: 2007-02-12 12:23:56 -0800 (Mon, 12 Feb 2007)
Log Message:
-----------
added Verify.getBoolean(boolean falseFirst) for saswat
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/src/gov/nasa/jpf/jvm/abstraction/symmetry/Threads.java
trunk/test/gov/nasa/jpf/peterd_tests/Peterson.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/jvm/choice/CustomBooleanChoiceGenerator.java
trunk/test/gov/nasa/jpf/peterd_tests/PetersonStatic.java
trunk/test/gov/nasa/jpf/peterd_tests/PetersonStatic2a.java
trunk/test/gov/nasa/jpf/peterd_tests/PetersonStatic2b.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-14 01:28:25
|
Revision: 250
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=250&view=rev
Author: pcmehlitz
Date: 2007-02-13 17:28:13 -0800 (Tue, 13 Feb 2007)
Log Message:
-----------
* updated classpath to include extensions/cv
* added an 'vm.store_steps' property to explicitly control if we have to store
transition steps. Even if there is no reporter with a 'trace' topic, there might
be listeners out there requiring the complete path info (like the SafetyAutomaton)
* a bad hot-fix for the ChoiceTracker, to avoid 'NONE' choices in the trace of
ui model checking. Need to find a generic way to do filtering, or re-add the UIActionTracker.
Maybe a generic "null" choice is the way to go
Modified Paths:
--------------
trunk/.classpath
trunk/default.properties
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/tools/ChoiceTracker.java
trunk/src/gov/nasa/jpf/util/Inspector.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-18 07:17:06
|
Revision: 257
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=257&view=rev
Author: pcmehlitz
Date: 2007-02-17 23:16:24 -0800 (Sat, 17 Feb 2007)
Log Message:
-----------
* intercept Object.wait() in native peer, so that we don't always get the Object.wait() as the
insn that causes the fatal Object.wait(long) in a deadlock
* had to slightly change ElementInfo.block() so that it sets the lockRef before the thread
gets blocked. Otherwise we can't find out about the object in the VMListener.notifyThreadBlocked()
* added some more source getters in Instruction. This really gets messy and needs to be
cleaned up
* with all that, finally gave the DeadLockAnalyzer deadlock.format=essential a first run.
Looking really good, even though the reporting certainly can be still polished
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/tools/DeadlockAnalyzer.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-23 08:59:22
|
Revision: 260
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=260&view=rev
Author: pcmehlitz
Date: 2007-02-23 00:58:59 -0800 (Fri, 23 Feb 2007)
Log Message:
-----------
* added a first version of the inverse state space spec for state machines: PathConstraints
this thing defines sequences of events that - if not matched - cause the current choice to
be ignored. This uses a choiceGeneratorAdvanced() notification, during which we might
skip the choice
* the UGLY thing is that SCEventFromAlphabet generators have this nasty behavior of being
expanded on demand (which might be deferred in the presence of completion triggers), in which
case they have to be explicitly advanced in the StateMachine native peer (i.e. after its out
of SystemState's hands). Hence we have to refactor the notification in SystemState, but that's not
yet satisfactory. However, the current 'skip choice' mechanism is very questionable in
the context of trace replay, so this has to be changed anyways
Modified Paths:
--------------
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
trunk/src/gov/nasa/jpf/jvm/ChoiceGenerator.java
trunk/src/gov/nasa/jpf/jvm/SystemState.java
trunk/src/gov/nasa/jpf/util/script/ESParser.java
trunk/src/gov/nasa/jpf/util/script/ScriptElementContainer.java
Added Paths:
-----------
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/PathConstraint.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-02-26 07:40:57
|
Revision: 264
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=264&view=rev
Author: pcmehlitz
Date: 2007-02-25 23:40:55 -0800 (Sun, 25 Feb 2007)
Log Message:
-----------
* search.multiple_errors had an error - if we bail out of JVM.forward() with an UncaughtException
(this thing REALLY has to go away, I'm saying that since 3 years), we need to store the SystemState
or backtracking & continue does get out of sync (CG doesn't get properly backtracked)
* SystemState.setIgnored() can now also be called from a choiceGeneratorAdvanced() notification,
i.e. before we execute any code in this transition. Be aware that - even if it's possible - one
should not do any deferred CGs if that feature is used
* the big thing was rewriting the StateMachine so that 'completion' events are treated like
normal events, i.e. handled on the native peer / subclass side. This eliminates the need
for the imfamous non-consumed, and esp. the on-demand expanded SCEventFromAlphabet CGs. They
were just a nightmare, code is much cleaner now
* updated SimStateMachine to use this scheme
* fixed PathConstraints, added an ad hoc, greedy complement event ~<someevent> to better
suit flight rules, but the script syntax needs to be reworked
* added an 'choice.exclude' filter for the ChoiceTracker, to filter out things like
'completion' or 'NONE'
* updated UIInspector accordingly
Modified Paths:
--------------
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/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/PathConstraint.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/SystemState.java
trunk/src/gov/nasa/jpf/tools/ChoiceTracker.java
trunk/src/gov/nasa/jpf/util/script/ESParser.java
Removed Paths:
-------------
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/NullSCEventGenerator.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventFromAlphabet.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-01 07:45:55
|
Revision: 271
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=271&view=rev
Author: pcmehlitz
Date: 2007-02-28 23:45:54 -0800 (Wed, 28 Feb 2007)
Log Message:
-----------
* added simple java.util.concurrent.AtomicReferenceFieldUpdater replacement. It's apparently
used in BufferedInputStream. This thing doesn't do much else than the compareAndSet(), which
is trivial to implement on the peer side
* added a FieldInfo.getTypeClassInfo()
* it seems java.lang.reflect.Field was using the FieldInfo type name wrongly
* added a little more info to the error section printing in the ConsolePublisher
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
Added Paths:
-----------
trunk/env/jpf/java/util/concurrent/atomic/
trunk/env/jpf/java/util/concurrent/atomic/AtomicReferenceFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-01 23:57:03
|
Revision: 272
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=272&view=rev
Author: pcmehlitz
Date: 2007-03-01 15:56:54 -0800 (Thu, 01 Mar 2007)
Log Message:
-----------
* added a Types.getCanonicalTypeName(), to overcome the stupid "byte" vs. "[B
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileDescriptor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/Types.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-02 00:03:09
|
Revision: 273
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=273&view=rev
Author: pcmehlitz
Date: 2007-03-01 16:03:06 -0800 (Thu, 01 Mar 2007)
Log Message:
-----------
last commit got fired off prematurely, so here goes again
* added a Types.getCanonicalTypeName to overcome the "byte" vs. "[B" anomaly. This is now
used for lookup in ClassInfo.getClassInfo.
the FieldInfo still needs to be updated, since it still uses the "Ljava/lang/String;" notation,
causing a lot of superfluous name conversions (I guess that comes from BCEL)
* with that, fixed the AtomicReferenceFieldUpdater so that it can also handle arrays of
builtin types
* added a simple regtest for it
* ..and with that the BufferedInputStream should run - so I've added another reg test
for that one too
Modified Paths:
--------------
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/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/jpf.properties
Added Paths:
-----------
trunk/test/gov/nasa/jpf/jvm/TestAtomicReferenceFieldUpdater.java
trunk/test/gov/nasa/jpf/jvm/TestAtomicReferenceFieldUpdaterJPF.java
trunk/test/gov/nasa/jpf/jvm/TestBufferedInputStream.java
trunk/test/gov/nasa/jpf/jvm/TestBufferedInputStreamJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-07 04:55:13
|
Revision: 275
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=275&view=rev
Author: pcmehlitz
Date: 2007-03-06 20:55:09 -0800 (Tue, 06 Mar 2007)
Log Message:
-----------
* support for guarded completion triggers: added an 'wasGuardedCompletionStep' to the
StateMachine state space, which is set from the native peer (in checkStep)
* for guided MC (by means of scripts with option-less event sequences), we need to keep
track of which events (incl. param values) we have seen in which states, otherwise we
risk cutting a sequence short because of premature state matching (the infamous
"e(true); e(false)" example - Completion1.es). This per-state set is then used to
set a 'forceNewState' in the StateMachine state space
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/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
trunk/src/gov/nasa/jpf/tools/DeadlockAnalyzer.java
trunk/src/gov/nasa/jpf/util/script/EventGeneratorFactory.java
Added Paths:
-----------
trunk/extensions/statechart/examples/Completion1.es
trunk/extensions/statechart/examples/Completion1.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-09 19:16:08
|
Revision: 277
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=277&view=rev
Author: pcmehlitz
Date: 2007-03-09 11:16:05 -0800 (Fri, 09 Mar 2007)
Log Message:
-----------
* Ok, there are daemons out there - by chance discovered that running TestVMDeadlockJPF
from ant and explicitly via bin/javajpf yielded different results! Ant said Ok, javajpf
actually reported an error.
to make matters worse, the error was real - the artificial RUNSTART (justified by the
"max one CG per insn" constraint) in combination with the Thread.start() native peer
caused an assertion in ElementInfo.lock(), because nobody ever called
ThreadInfo.registerLockContender(ei). And to make that even worse, I now think that
Thread.start has to be a breaker (we had a createThreadStartCG in the SchedulerFactory,
but it was optional and returned null). I think the reason why it has to be a right mover
is that the freshly started thread might well do something (like starting another thread
that interacts with the starter) that causes one of the next insns in the starter to
become a right mover. The real trick with this is that we can't check for
ThreadInfo.isFirstStepInsn in RUNSTART, since it always will be the first insn, so the
block()/registerLockContender() is in Thread.start(), the lock(ti) is in RUNSTART :(
Still need a regression test for that
* finally did bite the bullet and created a 'RawTest' base for our raw tests. Still
it has to run outside JPF, but the main() driver was just too redundant. Now I just
have to update all raw tests to use that (so far, only TestVMDeadlock does)
* added simple asym lock and nested monitor lockout test cases to TestVMDeadlock
* fixed a small bug in ExecTracker, which gets into trouble if we skip insn logging
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/bytecode/RUNSTART.java
trunk/src/gov/nasa/jpf/tools/ExecTracker.java
trunk/test/gov/nasa/jpf/mc/TestVMDeadlock.java
trunk/test/gov/nasa/jpf/mc/TestVMDeadlockJPF.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/jvm/RawTest.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-21 00:32:03
|
Revision: 287
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=287&view=rev
Author: pcmehlitz
Date: 2007-03-20 17:31:59 -0700 (Tue, 20 Mar 2007)
Log Message:
-----------
* added CG statistics for the StateSpaceAnalyzer. Still leaves me with the
Thread map
* added some generic Misc methods to for list sorting and occurrence map creation
* used that to factorize StateSpaceAnalyzer
* renamed getMethod[Info] accessor in Instruction
Modified Paths:
--------------
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCConformanceListener.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/tools/CGMonitor.java
trunk/src/gov/nasa/jpf/tools/ExecTracker.java
trunk/src/gov/nasa/jpf/tools/IdleFilter.java
trunk/src/gov/nasa/jpf/tools/StateSpaceAnalyzer.java
trunk/src/gov/nasa/jpf/util/Misc.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/util/ElementCreator.java
trunk/src/gov/nasa/jpf/util/TwoTypeComparator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-21 23:50:07
|
Revision: 288
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=288&view=rev
Author: pcmehlitz
Date: 2007-03-21 16:50:05 -0700 (Wed, 21 Mar 2007)
Log Message:
-----------
* just a little renaming for demo purposes
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/tools/IdleFilter.java
trunk/test/gov/nasa/jpf/mc/TestRace.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-22 07:18:44
|
Revision: 290
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=290&view=rev
Author: pcmehlitz
Date: 2007-03-22 00:16:57 -0700 (Thu, 22 Mar 2007)
Log Message:
-----------
* reworked the PrciseRaceDetector a bit to provide more context info
and make it a bit faster. Also broke it a bit because the instance field
check isn't safe yet
* some cosmetic work on TestRace
* made Instruction.getSourceLocation stack trace conforming
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/tools/PreciseRaceDetector.java
trunk/test/gov/nasa/jpf/mc/TestRace.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-24 01:48:14
|
Revision: 292
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=292&view=rev
Author: pcmehlitz
Date: 2007-03-23 18:48:13 -0700 (Fri, 23 Mar 2007)
Log Message:
-----------
* some more oldclassic comments
* renamed JVM.getPath() into the more appropriate getClonedPath(), which has
quite some fan out (still have to check if all callers actually need a clone
* first stab on stateStored() notification. Had to add that to the SeachListener
for listeners that keep their own traces (like the DeadlockAnalyzer), in order to
make it work with HeuristicSearch.
There is still a bug in the way DeadlockAnalyzer uses this notification
* changed all direct SearchListener interfaces to be ListenerAdapter derived, so
that it becomes easier to extend the listener interfaces.
THIS MIGHT BREAK SOME CLIENT CODE - USE ListenerAdapter!
Modified Paths:
--------------
trunk/examples/issta2006/TestListener.java
trunk/examples/oldclassic.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/ModularTeacher.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCConformanceListener.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCModularTeacher.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCSafetyAutomaton.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCSafetyListener.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/SafetyAutomaton.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/SafetyListener.java
trunk/src/gov/nasa/jpf/GenericProperty.java
trunk/src/gov/nasa/jpf/ListenerAdapter.java
trunk/src/gov/nasa/jpf/PropertyListenerAdapter.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/VMState.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/report/Reporter.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/search/SearchListener.java
trunk/src/gov/nasa/jpf/search/SearchListenerMulticaster.java
trunk/src/gov/nasa/jpf/search/heuristic/BeamSearch.java
trunk/src/gov/nasa/jpf/search/heuristic/DefaultComparator.java
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicSearch.java
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicState.java
trunk/src/gov/nasa/jpf/tools/DeadlockAnalyzer.java
trunk/src/gov/nasa/jpf/tools/SearchMonitor.java
trunk/src/gov/nasa/jpf/tools/SearchStats.java
trunk/src/gov/nasa/jpf/tools/StateSpaceDot.java
trunk/src/gov/nasa/jpf/util/JPFRunner.java
trunk/test/gov/nasa/jpf/embedded/TestSearchListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-03-29 19:51:35
|
Revision: 297
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=297&view=rev
Author: pcmehlitz
Date: 2007-03-29 12:51:30 -0700 (Thu, 29 Mar 2007)
Log Message:
-----------
* refactored the StateMachine native peer to be merely a dispatcher. We now have
one host-VM NativeStateMachine instance per JPF StateMachine instance, with the
StateMachine.id value acting as the reference.
This is to support our beloved KC, where we need multiple StateMachines at a time
* added an MJIEnv.getReferredClassInfo(..)
Modified Paths:
--------------
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/src/gov/nasa/jpf/jvm/MJIEnv.java
Added Paths:
-----------
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: <pcm...@us...> - 2007-04-07 05:25:16
|
Revision: 302
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=302&view=rev
Author: pcmehlitz
Date: 2007-04-06 22:25:14 -0700 (Fri, 06 Apr 2007)
Log Message:
-----------
* apparently nobody is using Ant and build.xml anymore - there was a cyclic dependency
between MJIEnv and JPF_java_lang_Class. MJIEnv as a core class should of course not depend on
a library native peer. Moved the functionality of getReferredClassInfo into MJIEnv. Thanks Sergey!
will take care of the compiler warnings later
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.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