JavaPathFinder

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.

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.

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.

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.

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.

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.

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

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.

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
>

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Revision: 308
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=308&view=rev
Author:   pcmehlitz
Date:     2007-04-10 15:40:15 -0700 (Tue, 10 Apr 2007)

Log Message:
-----------
* rewoked the CoverageAnalyzer so that partially covered method bodies are
printed as fileLocation ranges, assuming that it is better to use Eclipse
for browsing than to print source snippets w/o comments

* Instruction.getSourceLocation() now just uses .getFileLocation(). Just a matter
of cleanup

Modified Paths:
--------------
    trunk/.classpath
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 309
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=309&view=rev
Author:   pcmehlitz
Date:     2007-04-12 14:27:00 -0700 (Thu, 12 Apr 2007)

Log Message:
-----------
* implemented explicit event sends via State.sendEvent(String,Object...) for both
StateMachine/NativeSateMachine and SimStateMachine

* implemented State.getEventId(), State.getEventArguments() to query event+args
of the event that got us into the current state (e.g. to be queried from
an entryAction, and used to send the next event)

these two should actually take care of (most of) the KC interfacing. Since KC praises
Moore state machines as the best thing since sliced bread, we should be able to map
this into our hierarchical scheme (there is always just one actve state), which left
us with explicit event sends

* StateMachine wasn't prepared to enter end states, i.e. still was looking for
a next event even if the entryAction sets the state to end state (why somebody would do
such a thing escapes me, but we want to be able to drive the whole machine from
within actions)

* added a little SendEvents1 test

* added sone newXX() methods for box types in MJIEnv

* ESParser didn't parse string literals correctly (StreamTokenizer returns it
as a '"' char, but with the sval set to the literal w/o quotes)

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/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
    trunk/src/gov/nasa/jpf/util/script/ESParser.java

Added Paths:
-----------
    trunk/extensions/statechart/examples/SendEvents1.es
    trunk/extensions/statechart/examples/SendEvents1.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 310
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=310&view=rev
Author:   pcmehlitz
Date:     2007-04-13 14:29:42 -0700 (Fri, 13 Apr 2007)

Log Message:
-----------
* added a bunch of reflection APIs to support running Junit through JPF

* added 'modifiers' to both ClassInfo and MethodInfo - but they are currently just
used for the reflection API, whereas they should replace the various 'isStatic', 'isPublic'
or whatever boolean fields

* fixed a bug in Class.getDeclaredMethod() - internally, we keep MethodInfos, i.e. don't
differentiate between methods and ctors. Externally (via the reflection API), we have to
do that

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.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.

Revision: 311
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=311&view=rev
Author:   pcmehlitz
Date:     2007-04-13 14:57:39 -0700 (Fri, 13 Apr 2007)

Log Message:
-----------
* NumberFormat.getInstance() was missing (defaults to NUMBER type)

* native Class.getMethod() failed on empty args list ??

Modified Paths:
--------------
    trunk/env/jpf/java/text/NumberFormat.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 313
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=313&view=rev
Author:   pcmehlitz
Date:     2007-04-14 19:19:37 -0700 (Sat, 14 Apr 2007)

Log Message:
-----------
* a hard days fight to make junit runnable under JPF, let's see..

* a bunch of missing reflection stuff

* didn't really handle Throwable.cause - it's sort of in now, but still
not fully compliant

* need to show native methods and Method.invoke as StackTraceElements, but both
are not on the stack (i.e. need to create them)

* InvocationTargetException is a pretty bad thing - we didn't handle it correctly (handle up to
the invoke() as the original exception, then wrap it into an InvocationTargetException), only
that ITXes store their cause differently (and override getCause). Nasty

* our StackTraceElement model class needs a toString()

* changed vm.halt_on_throw from a boolean into a string list with exception class name patterns

* File.getName() should only return base name 

Modified Paths:
--------------
    trunk/default.properties
    trunk/env/jpf/java/io/File.java
    trunk/env/jpf/java/lang/StackTraceElement.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Throwable.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.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.

Revision: 314
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=314&view=rev
Author:   pcmehlitz
Date:     2007-04-16 00:37:24 -0700 (Mon, 16 Apr 2007)

Log Message:
-----------
* reworked trace replay - the SystemState internal replay was too redundant with
the ChoiceSelector, and the double use of "vm.use_trace" (both create and replay)
was too confusing.

* removed all this stuff from SystemState

* storage is now done with the TraceStorer, and it can handle a number of store
conditions outside property_violations. This also solves the problem of storing
init traces (if no error was found). Use "trace.file=.." to specify trace file
names (there are also a bunch of other options like "trace.multiple"). Default
trace file name is "trace"

* replay is done via the ChoiceSelector, which now has the "choice.use_trace"
property

* added a simple SingSetMatcher, to get rid once and for all with the
"prefix vs. regexpr" lookup in class lists, field lists, method lists etc.
This one also handled wildcards in a more Java identifier friendly way
(wildcard is '*', the '.' is an ordinary char and can appear in the pattern)

Still need to convert potential users

Modified Paths:
--------------
    trunk/examples/ase2006/TestPartialTrace.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/ChoicePoint.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/jvm/Verify.java
    trunk/src/gov/nasa/jpf/search/Search.java
    trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java
    trunk/test/gov/nasa/jpf/mc/TestPartialTrace.java
    trunk/test/gov/nasa/jpf/mc/TestPartialTraceJPF.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/tools/TraceStorer.java
    trunk/src/gov/nasa/jpf/util/StringSetMatcher.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 316
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=316&view=rev
Author:   pcmehlitz
Date:     2007-04-17 13:09:43 -0700 (Tue, 17 Apr 2007)

Log Message:
-----------
* fixed bug with the java.text.Format initialization, causing only the last
created Format instance to be used. Forgot to call the super (Format) ctor
explicitly from the native peer, hence the 'id' handle never got updated.
Refactored native method into 'init0' calls, and added comments to all
relevant classes so that I don't forget it again

Modified Paths:
--------------
    trunk/env/jpf/java/text/DecimalFormat.java
    trunk/env/jpf/java/text/Format.java
    trunk/env/jpf/java/text/SimpleDateFormat.java
    trunk/env/jpf/java/util/concurrent/atomic/AtomicReferenceFieldUpdater.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DecimalFormat.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
    trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestNativePeer.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 322
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=322&view=rev
Author:   pcmehlitz
Date:     2007-04-20 22:17:31 -0700 (Fri, 20 Apr 2007)

Log Message:
-----------
* introduced java.lang.System model class, to better support system properties, which
can be initialized via JPF properties or just copied from the host VM. Downside is a
slightly increased startup time

* created first versions of InputStreamReader / OutputStreamWriter for the
byte / char conversion that makes Java IO so international and slow. It's
terribly inefficient in JPF since we can't do much buffering, so it's a per-byte/char
native call, but at least it should be sun.* free now.

* created gov.nasa.jpf.ConsoleOutputStream for System.out/err, which bypasses PrintStream
for better efficiency (vast majority of IO is still System.out.println())

* finally added basic support for String.format(..)

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java

Added Paths:
-----------
    trunk/env/jpf/gov/
    trunk/env/jpf/gov/nasa/
    trunk/env/jpf/gov/nasa/jpf/
    trunk/env/jpf/gov/nasa/jpf/ConsoleOutputStream.java
    trunk/env/jpf/java/io/InputStreamReader.java
    trunk/env/jpf/java/io/OutputStreamWriter.java
    trunk/env/jpf/java/lang/System.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_ConsoleOutputStream.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_InputStreamReader.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_OutputStreamWriter.java

Removed Paths:
-------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_PrintStream.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 325
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=325&view=rev
Author:   pcmehlitz
Date:     2007-04-23 00:48:38 -0700 (Mon, 23 Apr 2007)

Log Message:
-----------
* fixed both InputStreamReader & OutputStreamWriter to use block decode/encode. It's
still slow, but not braindead single char/byte conversion anymore. Still needs a lock
though

* little extension in DirectCallStackFrame.reset() - now we can reuse the frame
in loops from native methods

* finally created an example/testcase for an interative + recursive roundtrip
in TestNativePeer.testRoundtripLoop().
(JPF calls native, native repeatedly calls JPF, calls native). I hope that
doesn't cause all hell to break loose

* some more native String methods + tests

Modified Paths:
--------------
    trunk/env/jpf/java/io/InputStreamReader.java
    trunk/env/jpf/java/io/OutputStreamWriter.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_InputStreamReader.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_OutputStreamWriter.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
    trunk/src/gov/nasa/jpf/jvm/DirectCallStackFrame.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestNativePeer.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangString.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangStringJPF.java
    trunk/test/gov/nasa/jpf/jvm/TestNativePeer.java
    trunk/test/gov/nasa/jpf/jvm/TestNativePeerJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 326
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=326&view=rev
Author:   pcmehlitz
Date:     2007-04-23 22:40:07 -0700 (Mon, 23 Apr 2007)

Log Message:
-----------
* FileInputStream & FileOutputStream support - finally!
file data is stored in the real file system, which makes the mechanism
suitable for large files. The JPF side so far mainly stores the
file position and the status. Operations are implemented in a
slightly bent FileDescriptor.

NOTE: write still lacks some notion of file data hashing, so it *is* still
possible to have a false state match (but it's quite unlikely the
difference would be only in the file data)

* added a roundtrip test case for file IO and Writers/Readers

* slightly improved OutputStreamWriter for String output (no more
per operation alloc)
 

Modified Paths:
--------------
    trunk/env/jpf/java/io/FileDescriptor.java
    trunk/env/jpf/java/io/FileInputStream.java
    trunk/env/jpf/java/io/OutputStreamWriter.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileDescriptor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_OutputStreamWriter.java

Added Paths:
-----------
    trunk/env/jpf/java/io/FileOutputStream.java
    trunk/test/gov/nasa/jpf/jvm/TestFileIO.java
    trunk/test/gov/nasa/jpf/jvm/TestFileIOJPF.java

Removed Paths:
-------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileInputStream.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 327
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=327&view=rev
Author:   pcmehlitz
Date:     2007-04-27 00:12:23 -0700 (Fri, 27 Apr 2007)

Log Message:
-----------
first stab at serialization - ObjectInput/Outputstream works, even between a JVM and JPF.
I wouldn't consider it very stable yet, since our ObjectStreamClass compatibility is 
awfully fragile (esp. with respect to sun.misc.Unsafe and java.util.concurrency, which
are both used). At some point we should model ObjectStreamClass

* the SerializationConstructor is a hack around a hack - to be compatible, we need a
synthetic ctor that initializes only upwards from the first non-serializable superclass
and leaves everything below for explicit init via reflection. It's a bit lazy to do this
on the model side (the real Constructor is a final class) though

* lots of reflection related fixes (e.g. the static Field.getX/setX with null params)

* fix in the canonical class name (arrays use the L-dot notation)

* minimalistic support for Date (still requires a lot more to be performant)

* MessageDigest forwarding (finalize doesn't work yet?)

* AccessController didn't properly wrap exceptions

lots more  

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jpf/java/lang/reflect/Constructor.java
    trunk/env/jpf/java/lang/reflect/Field.java
    trunk/env/jpf/java/lang/reflect/Method.java
    trunk/env/jpf/java/security/AccessController.java
    trunk/env/jpf/sun/misc/Unsafe.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectStreamClass.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.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/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/Types.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java

Added Paths:
-----------
    trunk/env/jpf/gov/nasa/jpf/SerializationConstructor.java
    trunk/env/jpf/java/security/MessageDigest.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_SerializationConstructor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectInputStream.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_security_MessageDigest.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DateFormatSymbols.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_reflect_ReflectionFactory.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 329
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=329&view=rev
Author:   pcmehlitz
Date:     2007-04-27 15:44:58 -0700 (Fri, 27 Apr 2007)

Log Message:
-----------
* cleaned up the invoke instructions with respect to getting the callee

* shifted the MethodTracker to executeInstruction() notification

* put it to use with some Locale and TimeZone methods

but that still doesn't do it - we need to model Date to cut off the
sun.util.Calendar usage

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
    trunk/src/gov/nasa/jpf/tools/MethodTracker.java

Added Paths:
-----------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Locale.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_TimeZone.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 330
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=330&view=rev
Author:   pcmehlitz
Date:     2007-04-30 11:17:32 -0700 (Mon, 30 Apr 2007)

Log Message:
-----------
* the Eclipse search missed a JPF_java_lang_Class reference within MJIEnv,
which I most superfluously reintroduced (getReferredClassInfo() *is* in
MJIEnv nowadays)

* FileDescriptor didn't throw FileNotFoundException

* FileDescriptor access methods should check for fd != -1 and throw an
IOException if the file is closed

Modified Paths:
--------------
    trunk/env/jpf/java/io/FileDescriptor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileDescriptor.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.

Revision: 331
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=331&view=rev
Author:   pcmehlitz
Date:     2007-04-30 22:27:56 -0700 (Mon, 30 Apr 2007)

Log Message:
-----------
* serialization support for doubles (using Double.doubleToLongBits)

* more TimeZone, Calendar and Date forwarding (not yet safe due to Date's dual nature), esp.
Calendar needs a lot more to avoid sun.* stuff. TimeZone is a hack since it's an abstract class,
which we de-abstractify by means of it's peer

* String.equals wasn't null-safe

* temp file name support 

Modified Paths:
--------------
    trunk/env/jpf/java/io/File.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectInputStream.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_TimeZone.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java

Added Paths:
-----------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectOutputStream.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Calendar.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Date.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 332
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=332&view=rev
Author:   pcmehlitz
Date:     2007-05-02 01:05:01 -0700 (Wed, 02 May 2007)

Log Message:
-----------
* very very early ClassLoader support. Actually, we only support part of
the getResource(), and no user defined ClassLoaders yet (no link from
Class to ClassLoader yet), but that's good enough for simple file
resource lookup

* for that purpose, added a ClassInfo.getResource(), which has to
traverse the ClassPath itself because BCEL doesn't handle jar resources
(finds them, but there is no telling it is in a jar)

* ConsoleOutputStream wasn't null resilient

* added an AtomicLong compareAndSet, which is the basis for Random

* actually, there is an interesting question of how to handle
Random - it looks like we only optionally want this to turn into
CGs, because some apps would otherwise blow up

Modified Paths:
--------------
    trunk/env/jpf/gov/nasa/jpf/ConsoleOutputStream.java
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicLong.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java

Added Paths:
-----------
    trunk/env/jpf/java/lang/ClassLoader.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_ClassLoader.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 333
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=333&view=rev
Author:   pcmehlitz
Date:     2007-05-03 00:41:04 -0700 (Thu, 03 May 2007)

Log Message:
-----------
* InputStreamReader has to provide a ready()

* casting multi-dim array objects failed because of the / . type name confusion

* Random now uses the standard lib randomizing. Still need to do the optional
CG enumeration - THIS MIGHT BREAK SOME JPF EXAMPLE/TEST APPS!!

* StringBuffer wasn't null safe

* UNBELIEVABLE - apparently we never had growing DynamicXArrays, since there was
a freakish relict bug in the growth handling

Modified Paths:
--------------
    trunk/env/jpf/java/io/InputStreamReader.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_StringBuffer.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Array.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
    trunk/src/gov/nasa/jpf/jvm/Types.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
    trunk/src/gov/nasa/jpf/util/DynamicIntArray.java
    trunk/src/gov/nasa/jpf/util/DynamicObjectArray.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 335
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=335&view=rev
Author:   pcmehlitz
Date:     2007-05-04 16:57:23 -0700 (Fri, 04 May 2007)

Log Message:
-----------
* decode in InputStreamReader native peer has to be reset before using it in a new run

* DecimalFormatSymbols were missing some inits

* StackFrame.printStackframe() didn't work for synthetic methods (w/o classes)

CoverageAnalyzer has to be smarter about class dirs, so that it doesn't list classes twice (e.g. by
recursively descending into '.')

Modified Paths:
--------------
    trunk/env/jpf/java/io/InputStreamReader.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_InputStreamReader.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DecimalFormatSymbols.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/tools/CallMonitor.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 340
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=340&view=rev
Author:   pcmehlitz
Date:     2007-05-15 16:45:19 -0700 (Tue, 15 May 2007)

Log Message:
-----------
* leftover statemachine extensions from the demo

* NumericInstructionFactory that checks for classes to instrument

* StringSetMatcher convenience method for filters that use both
include and exclude sets

!! there seems to be a memory leak across repeated JPF invocations that shows up with the numeric test cases

Modified Paths:
--------------
    trunk/build.xml
    trunk/extensions/numeric/src/gov/nasa/jpf/numeric/NumericInstructionFactory.java
    trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
    trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumericJPF.java
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
    trunk/src/gov/nasa/jpf/Config.java
    trunk/src/gov/nasa/jpf/jvm/DefaultInstructionFactory.java
    trunk/src/gov/nasa/jpf/jvm/InstructionFactory.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
    trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
    trunk/src/gov/nasa/jpf/tools/AssertionProperty.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
    trunk/src/gov/nasa/jpf/util/StringSetMatcher.java
    trunk/test/gov/nasa/jpf/jvm/TestInsnInterceptionListener.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 341
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=341&view=rev
Author:   pcmehlitz
Date:     2007-05-15 23:05:30 -0700 (Tue, 15 May 2007)

Log Message:
-----------
* added an init(Config) call from the NativePeer ctor, to initialize
native peer classes. the method is optional, but should be implemented
if the native peer class (which is all static) has static fields that
might cause memory leaks during consecutive JPF runs (e.g. from junit
test cases)

* updated native peers accordingly, which fixed a rather serious leak
in JPF_java_lang_reflect_Method

* commented out the PeerDispatcher support, it seems superfluous since
reflection invocation got fast enough

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileDescriptor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_text_Format.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_security_MessageDigest.java
    trunk/src/gov/nasa/jpf/jvm/JVM.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.

Revision: 342
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=342&view=rev
Author:   pcmehlitz
Date:     2007-05-16 23:01:48 -0700 (Wed, 16 May 2007)

Log Message:
-----------
* native String.hashCode(), which makes a surprisingly huge difference in programs
that has a lot of Strings. I assume it's the step recording that came with 'statistics',
but that's not w/o relevance either. Side effect is that the original hashCode() of course
would have given the numeric bytecodes trouble, since it deliberatly overflows

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
    trunk/src/gov/nasa/jpf/jvm/Fields.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 343
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=343&view=rev
Author:   pcmehlitz
Date:     2007-05-21 16:58:35 -0700 (Mon, 21 May 2007)

Log Message:
-----------
* a kind of hack'ish workaround to avoid PrintStream initialization if all we need
is System.out / System.err (which are our very own ConsolePrintStreams). To preserve the
inheritance structure, ConsoleOutputStream is a PrintStream subclass, but unfortunately
the PrintStream(OutputStream) ctor checks for a 'null' argument, so we have to 
intercept the ConsoleOutputStream ctor in the peer. That means the PrintStream part of
it isn't initialized! Doesn't bother us as long as intercept all operations, which is
what we have this thing for anyways. Still, not very safe

* added getters for the StateMachine activeStates / nextActives sets, so that actions
that need to explicitly send events can check what to send (the "executable UML" dialect story)

* also added the interface to provide target states for explicit event sends, but that isn't
implemented yet on the native side

Modified Paths:
--------------
    trunk/env/jpf/gov/nasa/jpf/ConsoleOutputStream.java
    trunk/env/jpf/java/lang/System.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_ConsoleOutputStream.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.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


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 344
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=344&view=rev
Author:   pcmehlitz
Date:     2007-05-22 14:58:56 -0700 (Tue, 22 May 2007)

Log Message:
-----------
repository trouble again - seems at least two of my previous commits didn't make it
despite not showing an error. It's once more file renaming, not sure if Subversion or
Subclipse is the culprit. This is part 1 of the commit

* added branch coverage to the CoverageManager. It's not very polished yet, but at least we can
see which condition values are not executed

----------------------------------- previous commit message
* more work on static (re-)initialization of peer classes

* added a MethodInfoRegistry utility class. Since Method and Constructor are not inheritance related,
the best we can do to avoid code duplication is to factor this out

* added a RunRegistry/RunListener mechanism to help with dependencies between not inheritance related
peer classes. The problem is that the Class peer creates Constructor/
Method objects, so we either have to add Method and Class to the list of pre-initialized classes (bad, since
it means we have to make the dependencies explicit in JVM code that is otherwise not concerned about this), or
we have to come up with a general mechanism to detect re-initialization.

The general problem is that - wherever we use static fields (like in peers) - we have to be aware of
consecutive JPF runs (e.g. within a JUnit context), so we have to avoid memory leaks

* LogHandler didn't handle argument formatting

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DecimalFormat.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
    trunk/src/gov/nasa/jpf/util/LogHandler.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/util/MethodInfoRegistry.java
    trunk/src/gov/nasa/jpf/util/RunListener.java
    trunk/src/gov/nasa/jpf/util/RunRegistry.java

Removed Paths:
-------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_text_Format.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 346
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=346&view=rev
Author:   pcmehlitz
Date:     2007-05-23 10:08:14 -0700 (Wed, 23 May 2007)

Log Message:
-----------
* extended the StateMachine implementations so that events can be sent to specific
states. If no target state is provided, the event is sent to all active states. Semantics
are that in every step, the machine first looks for pending (sent) events for all
active states and creates a single CG from them. If there is no event pending (neither
sent to a state or to all), then the factory is used to obtain the next CG (from the
guidance script).

In scriptless mode, explicitly sent events are ignored, since the machine explores
all triggers for all active states anyways

With this mechanism, "executable UML" notations like KC (that use a number of concurrent
state machines communicating via explicit event sends) can be modeled as orthogonal
regions within the same master state. However, this still follows the run-to-completion
schema, i.e. these states advance synchronously (no concurrent execution)

still needs to be tested beyond SendEvent1 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/MJIEnv.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 347
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=347&view=rev
Author:   pcmehlitz
Date:     2007-05-24 01:06:02 -0700 (Thu, 24 May 2007)

Log Message:
-----------
* added a State.getMachine() accessor, which should be used with care since models should
be absolutely free of execution policy. This was necessary to obtain the set of active
states in our Unimod example

* finally started to implement the "vm.enumerate_random" option. Just nextInt() so far

* added a docu page with simple model checking examples. This needs to be more elaborated
to show how JPF differs from normal execution mode

Modified Paths:
--------------
    trunk/doc/Model_Checking_vs_Testing.html
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java

Added Paths:
-----------
    trunk/doc/sw_model_checking.html


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 348
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=348&view=rev
Author:   pcmehlitz
Date:     2007-05-25 15:33:15 -0700 (Fri, 25 May 2007)

Log Message:
-----------
* polished the "software model checking by example" page a bit, adding some graphs

* updated SVN access method in "Obtaining and Installing.."

* implemented Random.getBoolean for enumerate_random
this included a bug (missed re-init) in the Verify peer

* documented and updated the FixedPhone Java sources

* added a png for the FixedPhone

* updated default.properties with some new props

Modified Paths:
--------------
    trunk/default.properties
    trunk/doc/Obtaining_and_Installing_JPF.html
    trunk/doc/sw_model_checking.html
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
    trunk/extensions/statechart/examples/FixedPhone.java
    trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java

Added Paths:
-----------
    trunk/doc/JPF_files/graffle/sw-model-checking.graffle
    trunk/doc/JPF_files/state-graph-checking.png
    trunk/doc/JPF_files/state-graph-testing.png
    trunk/extensions/statechart/examples/FixedPhone.png


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 351
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=351&view=rev
Author:   pcmehlitz
Date:     2007-06-05 09:10:51 -0700 (Tue, 05 Jun 2007)

Log Message:
-----------
* don't change curEvent in StateMachine if it's only a completion (which does not require an event). The
implementation needs to be reworked though, since it's not backtracking/restore safe

* it's not UML, but with a slight modification, entryActions can now also do transitions. That's
to accomodate some of the "executable UML" dialects

* DFSHeuristic ctor was wrong

* CoverageAnalyzer should do some sanity checks on *.class files/jar entries before adding to
the set of analyzed classes

Modified Paths:
--------------
    trunk/doc/links.html
    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/src/gov/nasa/jpf/search/heuristic/DFSHeuristic.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 352
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=352&view=rev
Author:   pcmehlitz
Date:     2007-06-05 09:47:20 -0700 (Tue, 05 Jun 2007)

Log Message:
-----------
* active state carry over was wrong in last commit (only in case there was no
transition to a next state or end state, the current state has to be re-added
to the active set)

Modified Paths:
--------------
    trunk/bin/jpf.bat
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 354
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=354&view=rev
Author:   pcmehlitz
Date:     2007-06-06 23:46:45 -0700 (Wed, 06 Jun 2007)

Log Message:
-----------
* big overhaul of java.lang.Throwable - this was motivated by the runtime costs of
unconditionally creating StackTraceElement[] arrays to keep (more or less) the
execution snapshot at the time of the Throwable creation. Only that in 99% the
StackTraceElements are not explicitly used (only implicitly with x.printStackTrace())

Now we store this much more efficiently and less lossy as an int[] array containing
the global method ids and pc offsets

this should esp. make a difference in applications that do a lot of explorative
reflection lookup (which produces tons of NoSuchMethodExceptions etc.)

* since we now model Throwable, also streamlined the InvocationTargetException
(the cause/target mess)

* for that purpose, added an unconditional MethodInfo.globalId, which is just a running
index into a static ArrayList (as opposed to the previous IntTable)

* to offset the additional memory, finally removed the isStatic, isPublic, isSynchronized, isNative
attribute fields (which are all in modifiers anyways). Should actually save memory

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Throwable.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/report/ConsolePublisher.java

Added Paths:
-----------
    trunk/env/jpf/java/lang/Throwable.java
    trunk/env/jpf/java/lang/reflect/InvocationTargetException.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 355
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=355&view=rev
Author:   pcmehlitz
Date:     2007-06-07 16:16:04 -0700 (Thu, 07 Jun 2007)

Log Message:
-----------
* extended and updated the HeapTracker, which is now a PublisherExtension
and can report type allocation statistics. type filtering is now also
done with the StringSetMatcher (includes/excludes pattern)

the reason is that JavaSeq is broken with OutOfMemory, which must be some
standrad library modeling that's used from within Swing, and we have to
find out what it is. Unfortunately, Publisher isn't yet aware of OutOfMemory
(we need a property for that)

* PropertyListenerAdapter wasn't a PublisherExtension

* added the demo case to TestRandom

* updated the "Running JPF.." page, since -show is gone

Modified Paths:
--------------
    trunk/doc/Running_JPF.html
    trunk/src/gov/nasa/jpf/PropertyListenerAdapter.java
    trunk/src/gov/nasa/jpf/tools/HeapTracker.java
    trunk/test/gov/nasa/jpf/mc/TestRandom.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 356
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=356&view=rev
Author:   pcmehlitz
Date:     2007-06-08 19:12:25 -0700 (Fri, 08 Jun 2007)

Log Message:
-----------
* OUTCH - apparently, at least the Eclipse compiler does change slot types, and we didn't
reset the reference flag when setting long values. This caused JavaSeq to run into an
OutOfMemoryError that was cause by the mark phase (trying to set the mark bit for a
ridiculously large reference value). That was a tough one to debug

* publishFinished even if we run out of memory - there might be listeners configured
that give us a better idea how far we got

Modified Paths:
--------------
    trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 357
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=357&view=rev
Author:   pcmehlitz
Date:     2007-06-12 16:19:00 -0700 (Tue, 12 Jun 2007)

Log Message:
-----------
* the big change is that statechart guidance scripts are now instance (field) based, i.e.
we don't use the class names anymore to look up events. This was required because
the executable UML dialects require multiple instances of the same state (which are
'state machines' in their notation), and we would not have been able to write
guidance scripts for that. Recursive lookup through the hierarchy chain of states
still applies.

* to extend this, we now can also have arrays of states, which are named by
appending the subscript (in square brackets) to the array name. Also added a
little Array1 example for this

* a guidance script SECTION can now how have a comma separated list of IDs, to
specify event sequences for unrelated states

* added a preliminary (and very raw) guidance script documentation file

* the extension/statechart/build.xml was broken because we have an inverted
dependency chain. That's bad, and the fix in build.xml is bad too, but it
will take some time to reshuffle things, and the problem does not occur inside
Eclipse anyways

There soon will be a more elaborate 'jpfESAS' example for the statechart extension

Modified Paths:
--------------
    trunk/default.properties
    trunk/extensions/statechart/build.xml
    trunk/extensions/statechart/doc/translation-rules.txt
    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_State.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/statechart/examples/FixedPhone.es
    trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/PathConstraint.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/util/script/ESParser.java
    trunk/src/gov/nasa/jpf/util/script/Section.java
    trunk/src/gov/nasa/jpf/util/script/StringSetGenerator.java

Added Paths:
-----------
    trunk/extensions/statechart/doc/guidance-scripts.txt
    trunk/extensions/statechart/examples/Array1.es
    trunk/extensions/statechart/examples/Array1.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 365
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=365&view=rev
Author:   pcmehlitz
Date:     2007-06-20 15:45:38 -0700 (Wed, 20 Jun 2007)

Log Message:
-----------
* the big change is an overhaul and completion of the Stackframe attribute system.
attribute references for locals and operands are only added on demand, i.e. are
not allocated by default. Once they are there, xLOAD/xSTORE and all the operand stack
ops update attributes automatically (i.e. copy between stack and operands etc.). Using
the attributes needs more testing though

* this required some changes in the StackFrame interface (as exposed by ThreadInfo), to
better accomodate the xLOAD/xSTORE insns

* added some public StackFrame accessors for attributes and operand/local values

* various little bugs reg. Throwable (e.g. a missing native toString())

* changed the RawTest interface = we only support calling one test method at a time,
but with optional String/int/double/boolean parameters. This also wraps InvocationTargetExceptions
into RuntimeExceptions, so that RawTest main() methods don't have to declare exception anymore.
Updated a bunh of tests accordingly

* some obsolete Debug cleanup

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Throwable.java
    trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
    trunk/src/gov/nasa/jpf/jvm/DirectCallStackFrame.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/KernelState.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/Verify.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ALOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ASTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DLOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DSTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FLOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FSTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ILOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ISTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LLOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LSTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LocalVariableInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/NEW.java
    trunk/test/gov/nasa/jpf/jvm/RawTest.java
    trunk/test/gov/nasa/jpf/jvm/TestFileIO.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangString.java
    trunk/test/gov/nasa/jpf/jvm/TestNativePeer.java
    trunk/test/gov/nasa/jpf/jvm/TestNativePeerJPF.java
    trunk/test/gov/nasa/jpf/mc/TestRace.java
    trunk/test/gov/nasa/jpf/mc/TestRandom.java
    trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java
    trunk/test/gov/nasa/jpf/mc/TestVMDeadlock.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 381
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=381&view=rev
Author:   pcmehlitz
Date:     2007-06-21 23:09:09 -0700 (Thu, 21 Jun 2007)

Log Message:
-----------
* fix for the famous "Oksana bug" - due to the (bad) nature of the heap symmetry (DynamicMapIndex),
there actually were situations where the InvokeVirtual method caching did not work. It required the
same INVOKEVIRTUAL insn to get the same reference value for different objects, which in turn
requires the same allocation insn for different objects. Alternatively, any combination of
DynamicMapIndex inputs causing the same reference value (but that's probably even harder).

now we cache the callee ClassInfo. Slightly slower, but safe, and still saves us the (recursive) method
lookup if it's a match

* created a TestMethod test case, which in turn required to implement Runtime.gc() to force a GC

* extended the ObjectTracker so that invokes and gets are only printed as an option

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Runtime.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
    trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
    trunk/test/gov/nasa/jpf/jvm/TestMethod.java
    trunk/test/gov/nasa/jpf/jvm/TestMethodJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 395
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=395&view=rev
Author:   pcmehlitz
Date:     2007-06-26 17:15:59 -0700 (Tue, 26 Jun 2007)

Log Message:
-----------
* first installment of the Annotation replacement. We now don't use the real annotations anymore,
but model them as AnnotationInfo (created from bcel AnnotationEntries). The main reason for this is
to avoid having to put model types (like the statechart @Params) in the CLASSPATH.

AnnotationLoader/LoadedAnnotations are gone.

reflection support for Annotations (i.e. use in the application) still needs to be done. For now
we are mostly concerned about using annotations to specify JPF properties.

* updated bcel to the latest and greatest for the annotation support

* extended the ObjectTracker to check for @NonShared annotations - if a monitored object that has such
a class annotation is called or modified in another thread than its creator, we report a property
violation

* added a simple TestAnnotationProperties to the regression tests

* factored AnnotationSupport into a InfoObject class, which is the root for ClassInfo, MethodInfo, FieldInfo

* added a generic TestJPF.runJPFError() method

* added some post exec info to MONITOR instructions

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/lib/bcel.jar
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/filter/IgnoresFromAnnotations.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/filter/IncludesFromAnnotations.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/MONITOREXIT.java
    trunk/src/gov/nasa/jpf/tools/ExecTracker.java
    trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
    trunk/test/gov/nasa/jpf/jvm/TestJPF.java

Added Paths:
-----------
    trunk/env/jpf/gov/nasa/jpf/NonShared.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/InfoObject.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LockInstruction.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotationProperties.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotationPropertiesJPF.java

Removed Paths:
-------------
    trunk/src/gov/nasa/jpf/jvm/AnnotationLoader.java
    trunk/src/gov/nasa/jpf/jvm/LoadedAnnotations.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 403
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=403&view=rev
Author:   pcmehlitz
Date:     2007-06-27 12:50:33 -0700 (Wed, 27 Jun 2007)

Log Message:
-----------
* added a @Const annotation, together with a +ot.check_const option for the
ObjectTracker. It checks for PUTFIELDS from @Const marked methods

we could also do this deep, which would be cool

* restructured the ObjectTracker to make it a bit more generic

* extended the TestAnnotation regression tests for it

* yet again - some output formatting to enable source links from an Eclipse console

* some update in the TestNumeric reg tests (no throws in main())

Modified Paths:
--------------
    trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
    trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumericJPF.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotationProperties.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotationPropertiesJPF.java

Added Paths:
-----------
    trunk/env/jpf/gov/nasa/jpf/Const.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 405
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=405&view=rev
Author:   pcmehlitz
Date:     2007-06-27 14:00:36 -0700 (Wed, 27 Jun 2007)

Log Message:
-----------
* added .../test and .../examples subdirs for extension/symbc

Modified Paths:
--------------
    trunk/.classpath

Added Paths:
-----------
    trunk/extensions/symbc/examples/
    trunk/extensions/symbc/test/


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 419
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=419&view=rev
Author:   pcmehlitz
Date:     2007-06-28 16:31:08 -0700 (Thu, 28 Jun 2007)

Log Message:
-----------
* basic field attributes. arrays still need to be done

* forgot to propagate attributes in RETURN insns. not yet tested for long slots

* added a reg test for attribute propagation. does not cover statics or longs yet

* some more attribute accessors in ThreadInfo, icluding versions that do not
clone the top frame, which isn't necessary of we also changed a local/operand value

* added link to the practicioners guidebook

Modified Paths:
--------------
    trunk/doc/JPF_Related_Papers.html
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/Fields.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GETSTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IRETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/RETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 422
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=422&view=rev
Author:   pcmehlitz
Date:     2007-06-29 15:19:25 -0700 (Fri, 29 Jun 2007)

Log Message:
-----------
* tested and fixed long/double attributes. There is a snag - we have to decide whether to store
the attribute on the first or the second word (attributes for frames are kept per-slot, since
we don't have type info at all the bytecode ops). Since the StackFrame.getLocalVariableIndex() 
returns the lower index, we choose this one. But that means we have to explicitly use
setLongOperandAttr()/getLongOperandAttr() to access double word attributes

* added the corresponding accessors to ThreadInfo

* extended TestAttrs with statics and doubles

* added two more SystemState attributes: 'isForced' means we always treat this as a new state,
'retainAttributes' means we don't reset the attributes at each nextSucessor() call (i.e. Listeners
can switch matching on/off). Also made the existing attributes mutually exclusive (isForced/isIgnored,
isInteresting/isBoring). Added accessors in both SystemState and JVM 

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/SystemState.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/D2I.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/D2L.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DRETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/I2D.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/I2L.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/L2D.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LRETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 424
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=424&view=rev
Author:   pcmehlitz
Date:     2007-07-02 13:39:27 -0700 (Mon, 02 Jul 2007)

Log Message:
-----------
* added a GenericInstructionFactory, and refactored NumericInstructionFactory accordingly. Rationale is
to simplify creation of extensions that have their own execution modes (like various flavors of
symbolic execution) 

Modified Paths:
--------------
    trunk/extensions/numeric/src/gov/nasa/jpf/numeric/NumericInstructionFactory.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 434
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=434&view=rev
Author:   pcmehlitz
Date:     2007-07-10 19:07:47 -0700 (Tue, 10 Jul 2007)

Log Message:
-----------
* refactored the InvokeInstruction observability, esp. the getArgumentValues(), which was broken for
MJI methods. The problem is that NativePeer.executeMethod() returns with the callers stack modified
(args popped, return pushed), so an instructionExecuted had no way to determine what the call args
were. The current way of using the static NativePeer cache is the lesser of n evils, since it shouldn't
impose too much performance penalty to normal insns. Still this behavioral combinatorial snake pit of
instance/static JPF/MJI pre-/post- exec notification is not nice. There are probably some other
insns out there (fields) that still have to be made consistent too

* added some tests for this

* to aggravate this, added an INVOKECG pseudo-insn that can be used to obtain a method to call
from a InvocationCG, with an Invocation being the abstraction of a call. This will be used esp.
in drivers that require other entries than main() (like the upcoming thread-safe symbolic execution)

Modified Paths:
--------------
    trunk/extensions/numeric/src/gov/nasa/jpf/numeric/NumericInstructionFactory.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicListener.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/NativePeer.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/SystemState.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
    trunk/src/gov/nasa/jpf/tools/CallMonitor.java
    trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java
    trunk/src/gov/nasa/jpf/tools/MethodTracker.java
    trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
    trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
    trunk/src/gov/nasa/jpf/jvm/choice/InvocationCG.java
    trunk/src/gov/nasa/jpf/util/Invocation.java
    trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestInvokeListener.java
    trunk/test/gov/nasa/jpf/jvm/TestInvokeListener.java
    trunk/test/gov/nasa/jpf/jvm/TestInvokeListenerJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 435
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=435&view=rev
Author:   pcmehlitz
Date:     2007-07-11 16:34:02 -0700 (Wed, 11 Jul 2007)

Log Message:
-----------
* wow, bug in Class.asSubclass(), which caused JUnit 4.3 to fail. Amazing how long this can
go undetected. Added related regression tests

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 439
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=439&view=rev
Author:   pcmehlitz
Date:     2007-07-16 17:35:33 -0700 (Mon, 16 Jul 2007)

Log Message:
-----------
* the MethodInfo caching in VirtualInvocation was still broken (in case the callee ClassInfo was
not different, the lastObj reference was not updated). How hard can it be..

* all the explicit MethodInfo creators have to use the InstructionFactory, which for this purpose
had to be extended with a generic create(clsName). Be aware of that users have to initailze these
Instruction objects explicitly!

There are probably still some explicitly created Instruction objects that don't use the factory,
but at least the reflection call stub should do

Modified Paths:
--------------
    trunk/extensions/cv/src/gov/nasa/jpf/cv/AssertionFilteringListener.java
    trunk/src/gov/nasa/jpf/jvm/DefaultInstructionFactory.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/InstructionFactory.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFEQ.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFGE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFGT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFLE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFLT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFNE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFNONNULL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFNULL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPEQ.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPNE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPEQ.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPNE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKEINTERFACE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKEVIRTUAL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/NEW.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/NOP.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
    trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 447
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=447&view=rev
Author:   pcmehlitz
Date:     2007-07-19 10:17:13 -0700 (Thu, 19 Jul 2007)

Log Message:
-----------


Modified Paths:
--------------
    trunk/.classpath
    trunk/examples/Racer.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ALOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ANEWARRAY.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ASTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/BIPUSH.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DLOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DSTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FLOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FSTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GETSTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GOTO.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GOTO_W.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IINC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ILOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INSTANCEOF.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKEINTERFACE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ISTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/JSR.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/JSR_W.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LDC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LDC2_W.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LDC_W.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LLOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LOOKUPSWITCH.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LSTORE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/MULTIANEWARRAY.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/NEW.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/NEWARRAY.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/RET.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/SIPUSH.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/TABLESWITCH.java
    trunk/src/gov/nasa/jpf/util/Invocation.java

Added Paths:
-----------
    trunk/examples/launch/
    trunk/examples/launch/basic-racer-test.launch
    trunk/examples/launch/basic-racer.launch
    trunk/examples/launch/basic-random-test.launch
    trunk/examples/launch/basic-random.launch
    trunk/examples/launch/conc-0-RA-test.launch
    trunk/examples/launch/conc-1-RA.launch
    trunk/examples/launch/conc-2-RA_da.launch
    trunk/examples/launch/conc-3-lockorder.launch
    trunk/examples/launch/conc-4-ms.launch
    trunk/examples/launch/conc-5-nml.launch
    trunk/examples/launch/conc-6-race.launch
    trunk/examples/launch/conc-7-race-eraser.launch


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 448
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=448&view=rev
Author:   pcmehlitz
Date:     2007-07-19 11:00:17 -0700 (Thu, 19 Jul 2007)

Log Message:
-----------
* first beginnings of the "symbolic threadsafety" execution mode

* added a CodeBuilder to solve the offset/position initialization problem
when creating synthetic methods

Added Paths:
-----------
    trunk/extensions/symts/
    trunk/extensions/symts/src/
    trunk/extensions/symts/src/gov/
    trunk/extensions/symts/src/gov/nasa/
    trunk/extensions/symts/src/gov/nasa/jpf/
    trunk/extensions/symts/src/gov/nasa/jpf/ts/
    trunk/extensions/symts/src/gov/nasa/jpf/ts/GETFIELD.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFEQ.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNONNULL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNULL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESPECIAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKEVIRTUAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/PUTFIELD.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/
    trunk/extensions/symts/test/gov/
    trunk/extensions/symts/test/gov/nasa/
    trunk/extensions/symts/test/gov/nasa/jpf/
    trunk/extensions/symts/test/gov/nasa/jpf/ts/
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/jvm/CodeBuilder.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 449
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=449&view=rev
Author:   pcmehlitz
Date:     2007-07-22 22:58:52 -0700 (Sun, 22 Jul 2007)

Log Message:
-----------
* basic framework for symbolic threadsafe test generation

* had to turn some JVM methods into protected, probably more to follow

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/GETFIELD.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/PUTFIELD.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/util/Invocation.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 456
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=456&view=rev
Author:   pcorina
Date:     2007-07-24 19:36:56 -0700 (Tue, 24 Jul 2007)

Log Message:
-----------
added choco decision procedure:
http://choco.sourceforge.net/

Modified Paths:
--------------
    trunk/.classpath

Added Paths:
-----------
    trunk/choco-1_2_04.jar


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 458
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=458&view=rev
Author:   pcmehlitz
Date:     2007-07-26 12:00:46 -0700 (Thu, 26 Jul 2007)

Log Message:
-----------
* some core changes to make VM and bytecode subclassing easier

* got the TSVM/TestCandidate/TestType/Listener structure for the symbolic threadsafety exec
in place. NOT FUNCTIONAL YET - now I have to put the branch CGs back in place, and
settle on an exit strategy for test case detection

Modified Paths:
--------------
    trunk/examples/ase2006/Optimizer.java
    trunk/examples/issta2006/TestListener.java
    trunk/examples/issta2006/TestSearchMonitor.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java

Removed Paths:
-------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/GETFIELD.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESPECIAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKEVIRTUAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/PUTFIELD.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 460
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=460&view=rev
Author:   pcmehlitz
Date:     2007-07-30 16:57:02 -0700 (Mon, 30 Jul 2007)

Log Message:
-----------
* added the missing IfInstructions for the TS extension, delegating the insn execution
(to the TSVM. in absence of a better place). Caused some suboptimal refactoring of
base class method attributes, but that still looks better than to retrict the type
of listener that can be used in conjunction with the derived bytecodes.

* the Instruction.getNext(ThreadInfo) was outdated, we don't purge stackframes anymore
on System.exit

* added a very incomplete TestJavaLangSystem reg test

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFEQ.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNONNULL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNULL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFEQ.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFGE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFGT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFLE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFLT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFNE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFNONNULL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IFNULL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPEQ.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPNE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPEQ.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLT.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPNE.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java

Added Paths:
-----------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPEQ.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPNE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPEQ.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPNE.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangSystem.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangSystemJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 461
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=461&view=rev
Author:   pcmehlitz
Date:     2007-07-30 17:15:49 -0700 (Mon, 30 Jul 2007)

Log Message:
-----------
* always good to look twice - since the 'executeBothBranches' is so generic, why not
put it as a protected method in IfInstruction itself, so that we can delegate in
the overloaded execute() methods without a need for a caset, and within the same
package, i.e. without exposing critical instruction state like 'conditionValue'

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFEQ.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNONNULL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNULL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPEQ.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPNE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPEQ.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPNE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 465
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=465&view=rev
Author:   pcmehlitz
Date:     2007-08-01 16:35:22 -0700 (Wed, 01 Aug 2007)

Log Message:
-----------
* added a generic Trace / TraceElement pair to ease creation of property/application
specific traces from listeners. This is mainly factorizes the backtracking, including
state matching (i.e. reverting matched transitions)

* used this to do the TSVM trace over field access & lock ops (classical example of
property specific trace). Not completely integrated yet.

* added simple synchronization filter, but still needs to be extended towards
synchronized methods, which might require some refactoring

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/util/Trace.java
    trunk/src/gov/nasa/jpf/util/TraceElement.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 474
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=474&view=rev
Author:   pcmehlitz
Date:     2007-08-03 13:59:24 -0700 (Fri, 03 Aug 2007)

Log Message:
-----------
* next stab on InvokeInstruction.getArgumentValues() - this is a never ending story, with all it's
corner cases (native/bc pre/post exec, overlayed direct calls like clinit, exceptions etc.)

* added a Instruction.isCompleted(ti) so that listeners can check in instructionExecuted() if
the thing is actually done, or we will come back to it (CGs, direct call overlays like clinit
or preconds)

* for that, added some more stack accessors to ThreadInfo

* did a stupid rename of ThreadInfo.top() to getTopFrame() for consistencies sake, but wasn't aware
of the huge fan out (lots of changed classes)

* slightly enhanced the CallMonitor (depth, tid, isCompleted)

* some TSVM changed to do real parameter object initialization, to avoid NPEs and the like when
executing test methods. Not yet functional

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IADD.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IAND.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IDIV.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IFEQ.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IFGE.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IFGT.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IFLE.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IFLT.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IFNE.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IF_ICMPGE.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IF_ICMPGT.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IF_ICMPLE.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IF_ICMPLT.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IINC.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IMUL.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INEG.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/bytecode/IOR.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IREM.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/ISUB.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/IXOR.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/NativePeer.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/tools/CallMonitor.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 478
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=478&view=rev
Author:   pcmehlitz
Date:     2007-08-06 12:22:48 -0700 (Mon, 06 Aug 2007)

Log Message:
-----------
* need to "internalize" state/sent-event pairs, to enable state matching if we send
the same event over again, and that's the only change in the JPF state space. If we just
create new PendingEvent instances, this would never match. We need to check for
multiple occurrences of the same PendingEvent anyways

the trick we do is that we keep the PendingEvent instances in the target state, and
just mark them as processed / re-enable them on subsequent sends. That way, we save
a static HashMap (which would need to be reset on every JPF run)

this isn't yet symmetrical with respect to event order yet

* moved the send event logging into native - no need to have StringBuffers and all that
on the model side

* added a little reminder assertion if we transition into a State instance that wasn't declared
'final'. Still need to explore if I might silently re-initialize in this case
(we still need to check for multiple substate adds anyways)

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/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java

Added Paths:
-----------
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEvent.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 499
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=499&view=rev
Author:   pcmehlitz
Date:     2007-08-08 23:02:40 -0700 (Wed, 08 Aug 2007)

Log Message:
-----------
a bunch of extensions that in the end were not needed for the TS extension, but
seem to be useful enough to keep them

* ClassInfo got refactored to allow reloading of classes, e.g. with a changed bytecode factory

* bytecode factory can be set explicitly

* ti.createAndThrowException checks if the VM handles it, and if it does so leaves the
exception alone. This is esp. useful to consistently handle explicit (thrown) and implicit
(VM created) exceptions, e.g. to backtrack when encountering certain exceptions

* the GenericBytecodeFactory can filter target classes based on if a class belongs to the
parent set of a configued 'leaf class', or the child set of a 'root class'

* lots of changes in the TS extension - it now does completely homogenous execution. The
mixed symolic/concrete mode was just a snake pit. static init is skipped, the VM backtracks
when it encounters an exception. There's probably still a ton of pseudo inits missing though
(to avoid NPEs on reference fields)

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/src/gov/nasa/jpf/Config.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DefaultInstructionFactory.java
    trunk/src/gov/nasa/jpf/jvm/InstructionFactory.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FieldInstruction.java
    trunk/src/gov/nasa/jpf/jvm/choice/InvocationCG.java
    trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java

Added Paths:
-----------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/ATHROW.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 509
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=509&view=rev
Author:   pcmehlitz
Date:     2007-08-10 16:04:58 -0700 (Fri, 10 Aug 2007)

Log Message:
-----------
* added a little escape analysis to the TS execution mode, keeping
track of PUTFIELDs that store references which can reach the test object

* with this, added a filter for methods that use a relevant reference
as argument, implemented this for INVOKEVIRTUAL and INVOKESPECIAL

all other methods are now skipped, except of simulating returns

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 511
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=511&view=rev
Author:   pcmehlitz
Date:     2007-08-13 14:25:13 -0700 (Mon, 13 Aug 2007)

Log Message:
-----------
* more TS mode changes: some missing INVOKEx interceptions, consistent ATHROW and VM.handleException
treatment (ATHROW should use the same criteria)

a real problem are skipping generic method calls, since we don't know about the expected type.
It's now using the heuristic that such a call is usually followed by a CHECKCAST, but that's
only empirical observation. Anyways, with this, TestUnprotectedRW works again

* added CHECKCAST.getTypeName() for better inspection

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/ATHROW.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 512
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=512&view=rev
Author:   pcmehlitz
Date:     2007-08-13 22:07:21 -0700 (Mon, 13 Aug 2007)

Log Message:
-----------
* forgot to add a bunch of TS bytecodes

* in TSVM, relevantRefs need to be reset for every new test method

* the lock update in the TSVM listener was broken

* removed the 'result' publishing, it's pointless since we don't go after
property violations

* for that, had to change/add some APIs to set publisher topics

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
    trunk/src/gov/nasa/jpf/report/Publisher.java
    trunk/src/gov/nasa/jpf/report/Reporter.java
    trunk/src/gov/nasa/jpf/report/XMLPublisher.java

Added Paths:
-----------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKECLINIT.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESPECIAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESTATIC.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKEVIRTUAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/NEW.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 514
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=514&view=rev
Author:   pcmehlitz
Date:     2007-08-14 16:36:34 -0700 (Tue, 14 Aug 2007)

Log Message:
-----------
* refactored TSVM to hoist nested types to toplevel (except of the listener),
which is better for extension

* encapsulate the TestCandidates in TestSubject, since it will depend on
the subject what has to be stored (it's created from there anyways). The
TSVM is not the right place to store this

* got started on a better reporting, but still needs to factorize the
test code generation better (standalone files, JPF driver, test method args)

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/Config.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java

Added Paths:
-----------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/AccessOp.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/RWSameFieldRace.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/RaceCandidate.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TestSubject.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 515
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=515&view=rev
Author:   pcmehlitz
Date:     2007-08-15 18:02:57 -0700 (Wed, 15 Aug 2007)

Log Message:
-----------
* first stab at TS test source generation, as part of a new reporting scheme that uses the
refactored design

* added some argument inspection to Invocation, including getting literal value representations

* added a RawTest.runAllTests() - now I just have to bite the bullet and convert all
raw tests into RawTest instances

Modified Paths:
--------------
    trunk/doc/ChoiceGenerators.html
    trunk/extensions/symts/src/gov/nasa/jpf/ts/RWSameFieldRace.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/RaceCandidate.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TestSubject.java
    trunk/src/gov/nasa/jpf/util/Invocation.java
    trunk/test/gov/nasa/jpf/jvm/RawTest.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.

Revision: 516
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=516&view=rev
Author:   pcmehlitz
Date:     2007-08-16 10:44:56 -0700 (Thu, 16 Aug 2007)

Log Message:
-----------
* reverted the 'final' modifier requirement for structural State fields in state machine
model classes. As a reminder - this came up because there was an application that stored
states in ordinary variable fields, which were not intended to define the composition of
the state machine (basically, state machines and controlled objects got folded into the
same State class).

'final' seemed to be a good idea at the time, since the statemachine structure is
supposed to be invariant, but it was way too easy to forget the modifier and end up with
a runtime exception, thus killing our "no overhead, more easy than drawing" argument. I
think those strange references are way too exotic to value higher than ease of use

if you really really need such reference variables, they have to be marked with a
@NoSubState annotation

* moved the annotation type defs into State - saves an import and doesn't make
sense outside anyways

* updated the models accordingly (though 'final' doesn't have to be removed)

Modified Paths:
--------------
    trunk/extensions/statechart/doc/translation-rules.txt
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_State.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/statechart/examples/FixedPhone.java
    trunk/extensions/statechart/examples/SendEvents1.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.java

Removed Paths:
-------------
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/Params.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 517
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=517&view=rev
Author:   pcmehlitz
Date:     2007-08-16 17:31:14 -0700 (Thu, 16 Aug 2007)

Log Message:
-----------
* LOG_HOST and LOG_PORT are now config settable

* minor printing glitch in GOTO (NPE)

* finally picked up the "Output" documentation, but the reporting system is still missing

Modified Paths:
--------------
    trunk/doc/Output.html
    trunk/src/gov/nasa/jpf/jvm/bytecode/GOTO.java
    trunk/src/gov/nasa/jpf/util/LogHandler.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 518
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=518&view=rev
Author:   pcmehlitz
Date:     2007-08-17 13:17:06 -0700 (Fri, 17 Aug 2007)

Log Message:
-----------
* Publisher instantiation was missing a redirection. The "jpf.report.publisher"
property should only inlcude symbolic names that have to have a corresponding
".class" entry, like
...
jpf.report.publisher=console
jpf.report.console.class=gov.nasa.jpf.report.ConsolePublisher
...

* finished the "Output" docu text, but still needs a class diagram

Modified Paths:
--------------
    trunk/default.properties
    trunk/doc/Output.html
    trunk/src/gov/nasa/jpf/report/Reporter.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 520
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=520&view=rev
Author:   pcmehlitz
Date:     2007-08-18 12:29:02 -0700 (Sat, 18 Aug 2007)

Log Message:
-----------
* fixed a bug in array instantiation via java.lang.reflect.Array - the array
class was initialized in slash-notation, whereas Java seems to use the
dot-notation. Refactored this to happen in DynamicArea.newArray(), since
the initialization is just adding it to the StaticArea and creating the
class object.

The Java type names are a mess!! (method sigs use slash, array types dots,
sometimes "[]" gets appended, sometimes'[' prepended, sometimes it's
typecodes ('I'), sometimes primitive names ("int")..)

* had to add a public static accessor for the StaticArea, since there is
no access path for all clients. BAD. but has to be revisited anyways when
reworking the Dynamicarea/StaticArea. at least it's consistent with
DynamicArea.getHeap()

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Array.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/StaticArea.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.

Revision: 521
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=521&view=rev
Author:   pcmehlitz
Date:     2007-08-20 18:28:58 -0700 (Mon, 20 Aug 2007)

Log Message:
-----------
* long overdue docu update. The extension pages are still placeholders. Extensions now
should have their own .../doc directory, with a .../doc/index.html as their main page.
Just like the rest of JPF

* finally, the UML CEV statechart example (in examples/jpfESAS), with lots of disclaimers.
Reads: THIS IS ONLY BASED ON PUBLICLY AVAILABLE INFO AND DOES NOT REPRESENT ACTUAL
NASA FLIGHT CODE

Modified Paths:
--------------
    trunk/doc/Extensibility.html
    trunk/doc/History_and_Credits.html
    trunk/doc/JPF_Related_Papers.html
    trunk/doc/JPF_files/JPF-mod.css
    trunk/doc/RegressionTests.html
    trunk/doc/about_us.html
    trunk/doc/home.html
    trunk/doc/navigation.html
    trunk/doc/news.html

Added Paths:
-----------
    trunk/doc/extensions.html
    trunk/doc/legal.html
    trunk/examples/jpfESAS/
    trunk/examples/jpfESAS/CEV_15EOR_LOR.java
    trunk/examples/jpfESAS/ErrorLog.java
    trunk/examples/jpfESAS/Failures.java
    trunk/examples/jpfESAS/README-ESAS.txt
    trunk/examples/jpfESAS/Spacecraft.java
    trunk/examples/jpfESAS/launch/
    trunk/examples/jpfESAS/launch/CEV-ascent-guards.launch
    trunk/examples/jpfESAS/launch/CEV-assumption.launch
    trunk/examples/jpfESAS/launch/CEV-interactive-sim.launch
    trunk/examples/jpfESAS/launch/CEV-las-defect-sim.launch
    trunk/examples/jpfESAS/launch/CEV-las-defect.launch
    trunk/examples/jpfESAS/launch/CEV-nominal-sim.launch
    trunk/examples/jpfESAS/launch/CEV-safehold.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless-bt.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless-constraints.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless.launch
    trunk/examples/jpfESAS/launch/CEV-tli-sim.launch
    trunk/examples/jpfESAS/launch/CEV-tli.launch
    trunk/examples/jpfESAS/launch/CV-assumption-1.launch
    trunk/examples/jpfESAS/launch/CV-assumptions-1-2.launch
    trunk/examples/jpfESAS/launch/CV-generate-assumption-1.launch
    trunk/examples/jpfESAS/launch/CV-generate-assumption-2.launch
    trunk/examples/jpfESAS/script/
    trunk/examples/jpfESAS/script/Assumption1.txt
    trunk/examples/jpfESAS/script/Assumption2.txt
    trunk/examples/jpfESAS/script/CEV_15EOR_LOR-ascent-guards.es
    trunk/examples/jpfESAS/script/CEV_15EOR_LOR-las-defect.es
    trunk/examples/jpfESAS/script/CEV_15EOR_LOR-las-sim.es
    trunk/examples/jpfESAS/script/CEV_15EOR_LOR-nominal.es
    trunk/examples/jpfESAS/script/CEV_15EOR_LOR-safehold.es
    trunk/examples/jpfESAS/script/CEV_15EOR_LOR-tli-sim.es
    trunk/examples/jpfESAS/script/CEV_15EOR_LOR-tli.es
    trunk/examples/jpfESAS/script/flightrules.ec
    trunk/examples/jpfESAS/script/generatedAssumption1
    trunk/examples/jpfESAS/script/generatedAssumption2
    trunk/extensions/cv/doc/
    trunk/extensions/cv/doc/index.html
    trunk/extensions/numeric/doc/
    trunk/extensions/numeric/doc/index.html
    trunk/extensions/statechart/doc/index.html
    trunk/extensions/statechart/doc/scripting.html
    trunk/extensions/statechart/doc/toolchain.graffle
    trunk/extensions/statechart/doc/toolchain.png
    trunk/extensions/statechart/doc/translation.html
    trunk/extensions/symbc/doc/
    trunk/extensions/symbc/doc/index.html
    trunk/extensions/symts/doc/
    trunk/extensions/symts/doc/index.html
    trunk/extensions/ui/doc/
    trunk/extensions/ui/doc/index.html

Removed Paths:
-------------
    trunk/extensions/statechart/doc/guidance-scripts.txt
    trunk/extensions/statechart/doc/translation-rules.txt


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 523
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=523&view=rev
Author:   pcmehlitz
Date:     2007-08-23 00:25:40 -0700 (Thu, 23 Aug 2007)

Log Message:
-----------
* INVOKECG isn't really an InvokeInstruction, it creates one. Subtle difference with
far reaching consequences for listeners on INVOKEs

* The generic Instruction.isCompleted(ti) didn't work for InvokeInstructions, since the
INVOKE is always still on the caller (i.e. lower) stack frame. Now the InvokeInstruction
overrides it, checking if the topframe pc is the first insn in the called method

* TSVM now falls back to the INVOKECG if it finds a test candidate. No need to
look for a different path for the same candidate, since the created test would be the same

* TSVM ignores all java.* exceptions, since those are most likely caused by placeholder
("symbolic") values

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/tools/CallMonitor.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 531
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=531&view=rev
Author:   pcmehlitz
Date:     2007-08-23 22:42:31 -0700 (Thu, 23 Aug 2007)

Log Message:
-----------
* refactoed the switch instructions, giving them a common baseclass, and providing an
executeAllBranches()

* added the switch insns to the TS set

* added the xSTORE xASTORE and IINC to the TS set - we don't want to track any values
other than references, and rather want to match more states

* fixed potential endless recursion in the way we create test objects. Still not
safe though

* had to move the VM.handleException into ThreadInfo.throwException(), otherwise
it wouldn't cover explicit throws. It's now object based, but performance shouldn't
be so important here

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESPECIAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESTATIC.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKEVIRTUAL.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LOOKUPSWITCH.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/TABLESWITCH.java
    trunk/src/gov/nasa/jpf/tools/CallMonitor.java

Added Paths:
-----------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/DASTORE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/DSTORE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IASTORE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/IINC.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/ISTORE.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/LOOKUPSWITCH.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TABLESWITCH.java
    trunk/index.html
    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.

Revision: 535
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=535&view=rev
Author:   pcmehlitz
Date:     2007-08-24 16:02:55 -0700 (Fri, 24 Aug 2007)

Log Message:
-----------
* the test object set in TSVM wasn't backtrackable, which of course leads to referencing objects
which are not there yet. We can't simply create new test objects upon each request because then
we have to somehow break endless recursion ("class Throwable { Throwable cause; .. }" )

* for that purpose, added a DynamicArea.getNext(ClassInfo ci, int startIdx) that returns
the next instance of the provided class from a given index (can also be used to iterate over
all instances of a certain class)

still the test object creation is the biggest problem for the TS mode. It remains to be seen
how many classes of false positives we can still filter out

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 536
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=536&view=rev
Author:   pcmehlitz
Date:     2007-08-24 16:41:02 -0700 (Fri, 24 Aug 2007)

Log Message:
-----------
* some minor bugs in the test source generation

* test src directory and jpf basedir to use are now ts.* properties

..and with that, the JulianDate test generation runs end-to-end! 

Modified Paths:
--------------
    trunk/extensions/symts/src/gov/nasa/jpf/ts/RWSameFieldRace.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
    trunk/extensions/symts/src/gov/nasa/jpf/ts/TestSubject.java
    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.

Revision: 538
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=538&view=rev
Author:   pcmehlitz
Date:     2007-08-29 23:26:42 -0700 (Wed, 29 Aug 2007)

Log Message:
-----------
* before AntlrWorks pulls me a leg again, I commit the current test infrastructure
it starts to work but still need some polishing, plus a lot more goals

PLEASE NOTE - this requires the Antlr 3.x runtime lib to compile

* added arrays to the AnnotationInfo

* moved the stuff that is supposed to be used from apps (that make explicit use of
JPF)  into .../app

ultimately, Verify should go there too, but still needs to be cleaned up

Modified Paths:
--------------
    trunk/.classpath
    trunk/bin/javajpf
    trunk/bin/jpf
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/util/StringSetMatcher.java
    trunk/src/gov/nasa/jpf/util/script/Event.java

Added Paths:
-----------
    trunk/app/
    trunk/app/gov/
    trunk/app/gov/nasa/
    trunk/app/gov/nasa/jpf/
    trunk/app/gov/nasa/jpf/Const.java
    trunk/app/gov/nasa/jpf/NonShared.java
    trunk/app/gov/nasa/jpf/Test.java
    trunk/lib/antlr-runtime-3.0.1.jar
    trunk/src/gov/nasa/jpf/test/
    trunk/src/gov/nasa/jpf/test/ArgList.java
    trunk/src/gov/nasa/jpf/test/CompareGoal.java
    trunk/src/gov/nasa/jpf/test/Goal.java
    trunk/src/gov/nasa/jpf/test/NoThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpec.java
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/src/gov/nasa/jpf/test/ThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/ValSet.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/src/gov/nasa/jpf/util/ExpandableStringReader.java
    trunk/src/gov/nasa/jpf/util/StringExpander.java
    trunk/test/gov/nasa/jpf/test/
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java

Removed Paths:
-------------
    trunk/env/jpf/gov/nasa/jpf/Const.java
    trunk/env/jpf/gov/nasa/jpf/NonShared.java
    trunk/src/gov/nasa/jpf/util/script/ExpandableStringReader.java
    trunk/src/gov/nasa/jpf/util/script/StringExpander.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 540
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=540&view=rev
Author:   pcmehlitz
Date:     2007-08-30 22:30:01 -0700 (Thu, 30 Aug 2007)

Log Message:
-----------
* some more type compatibility checks (also return type and goal type), but
we still need casts

not clear yet if this should happen while parsing, or during invocation

* added a generic RegexGoal, which matches ret.toString() against a regex - nice

* reminder comment in PUTSTATIC for the next Oksana bug - we can't shut off
class init from <clinits> (was there to avoid infinite recursion), since there
are rare cases where a PUTSTATIC from a <clinit> really initializes another class
(the imfamous synthetic "class$0" field.

Still needs a fix 

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java
    trunk/src/gov/nasa/jpf/test/CompareGoal.java
    trunk/src/gov/nasa/jpf/test/Goal.java
    trunk/src/gov/nasa/jpf/test/NoThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/src/gov/nasa/jpf/test/ThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/ValSet.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/RegexGoal.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 541
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=541&view=rev
Author:   pcmehlitz
Date:     2007-09-01 21:03:03 -0700 (Sat, 01 Sep 2007)

Log Message:
-----------
* added basic object creation (works recursive)

* changed arg/ret compatibility checks to be based on values, to enable casts that
are type/value compatible

* Class.getPackage() needs to be implemented

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/src/gov/nasa/jpf/test/ValSet.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/ObjectCreator.java
    trunk/src/gov/nasa/jpf/test/ObjectException.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 542
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=542&view=rev
Author:   pcmehlitz
Date:     2007-09-02 21:08:11 -0700 (Sun, 02 Sep 2007)

Log Message:
-----------
* added WithinGoal and modified grammar accordingly
still needs some type casting support

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/WithinGoal.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 545
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=545&view=rev
Author:   pcmehlitz
Date:     2007-09-04 17:21:07 -0700 (Tue, 04 Sep 2007)

Log Message:
-----------
* apparently one of the last commits broke the MethodTester with an unknown ObjectCreater.ctor.
Since I renamed it to 'TestContext', this should fix it

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/FieldReference.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/TestContext.java

Removed Paths:
-------------
    trunk/src/gov/nasa/jpf/test/ObjectCreator.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 546
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=546&view=rev
Author:   pcmehlitz
Date:     2007-09-05 12:28:59 -0700 (Wed, 05 Sep 2007)

Log Message:
-----------
* ARRAYLENGTH insn wasn't checking for NPEs

* File was missing isFile()

* better support for goal type conversion & runtime checking

* field refs in WithinGoals

* type checks & conversions on WithinGoal

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_File.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ARRAYLENGTH.java
    trunk/src/gov/nasa/jpf/test/CompareGoal.java
    trunk/src/gov/nasa/jpf/test/FieldReference.java
    trunk/src/gov/nasa/jpf/test/Goal.java
    trunk/src/gov/nasa/jpf/test/NoThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/RegexGoal.java
    trunk/src/gov/nasa/jpf/test/TestContext.java
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/src/gov/nasa/jpf/test/ThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/WithinGoal.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 547
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=547&view=rev
Author:   pcmehlitz
Date:     2007-09-05 16:32:30 -0700 (Wed, 05 Sep 2007)

Log Message:
-----------
* turned both targetArgs and callArgs into lists of ArgLists, so that we
can process subsets of all arg combinations. Syntax is like

  this(10|11) | this(20) . (1|2,3|4) | (42,43)

every ctor combination is tested with all call combinations 

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpec.java
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 549
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=549&view=rev
Author:   pcmehlitz
Date:     2007-09-06 11:24:59 -0700 (Thu, 06 Sep 2007)

Log Message:
-----------
* reorganized the cast support in TestContext a bit

* extended the grammar with generic collections (".., {..}|{..},..")

* basic casting support for collections (primitive arrays, List/ArrayList, Vector)

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/TestContext.java
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 553
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=553&view=rev
Author:   pcmehlitz
Date:     2007-09-07 13:07:49 -0700 (Fri, 07 Sep 2007)

Log Message:
-----------
* added a pre-invoke goal check, for goals that need to capture before/after states (incl target object)

* turned Goal into an abstract, since it's getting more and more public methods

* added a generic backdoor for new Goals w/o the need to modify the parser. The "satisfies" clause
now takes an id and an optional arglist, which are instantiated via the TestContext, which now really
becomes a factory for all sort of test things

* with that, implemented a simple MemoryGoal. It kind of works standalone, but since normal VMs
don't keep track of heap memory on a per object basis, the granularity is probably not enough. Makes
a good example of how to use JPF to be more precise

* added a generic "createObject" to Misc, to factorize the common case of looking up ctors, and
instantiating objects with various argument lists

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/CompareGoal.java
    trunk/src/gov/nasa/jpf/test/Goal.java
    trunk/src/gov/nasa/jpf/test/NoThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/RegexGoal.java
    trunk/src/gov/nasa/jpf/test/TestContext.java
    trunk/src/gov/nasa/jpf/test/TestSpec.g
    trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
    trunk/src/gov/nasa/jpf/test/TestSpecParser.java
    trunk/src/gov/nasa/jpf/test/ThrowsGoal.java
    trunk/src/gov/nasa/jpf/test/WithinGoal.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/src/gov/nasa/jpf/util/Misc.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/MemoryGoal.java
    trunk/src/gov/nasa/jpf/test/TestException.java

Removed Paths:
-------------
    trunk/src/gov/nasa/jpf/test/ObjectException.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 559
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=559&view=rev
Author:   pcmehlitz
Date:     2007-09-10 08:11:10 -0700 (Mon, 10 Sep 2007)

Log Message:
-----------
* weird - the multi-goal extension seem to not have made it into the last commit. Here it
is again: multiple goals per TestSpec, all checked in different executions

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 560
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=560&view=rev
Author:   pcmehlitz
Date:     2007-09-11 14:40:23 -0700 (Tue, 11 Sep 2007)

Log Message:
-----------
the grand scheme is to make the MethodTester run under JPF. For that we need a lot more reflection..

* added synthetic, on-the-fly creation of Annotation proxy classes, turning annotation entries into
field/accessor pairs. Some functionality resides in an actificial AnnotationProxyBase, so that we don't
have to generate too much code. And since it's not subject to verification, the code is actually
in a NativePeer

* added initialize(..) methods for ALOAD,GETFIELD so that we can instantiate them in synthetic methods

* added missing Array.get()

* added missing Class.getAnnotation() (Method/Field.getAnnotation() still missing, but the same)

* added MethodTester and MemoryGoal NativePeers, to facilitate execution under JPF. native peers are
the preferred way to add JPF specific behavior

* added a DynamicArea.getHeapSize() for statistical purposes

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Array.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ALOAD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IRETURN.java
    trunk/src/gov/nasa/jpf/test/Goal.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java

Added Paths:
-----------
    trunk/env/jpf/gov/nasa/jpf/AnnotationProxyBase.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_tools_MethodTester.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 561
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=561&view=rev
Author:   pcmehlitz
Date:     2007-09-11 16:35:26 -0700 (Tue, 11 Sep 2007)

Log Message:
-----------
* the missing Field/Method.getAnnotation()

* ..and the Class/Field/Method.getAnnotations() - it's not really correct yet, since we have to
distinguish between declared and inherited annotations for classes, but that should be rather
exotic

what's still missing for annotation modeling are enums

Modified Paths:
--------------
    trunk/env/jpf/java/lang/reflect/Field.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.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.

Revision: 562
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=562&view=rev
Author:   pcmehlitz
Date:     2007-09-12 12:09:22 -0700 (Wed, 12 Sep 2007)

Log Message:
-----------
* better support for Enums - added a ClassInfo.isEnum to easily identify enum const objects

* <sigh> had to add a "longjmp" exception (gov.nasa.jpf.jvm.ClinitRequired) to handle clinit
requests from deep inside of the stack, where we can't simply use a return value or even know
what the executed insn was that caused the request. This is for instance required if we reference
class fields & arrays of Annotation proxy objects (how obvious!). It's used in the
getAnnotation()/getAnnotations() methods

Not so nice.

Also refactored some of the repeatInvocation() handling into MJIEnv, since it's most likely
going to be used from native peer methods (the bytecodes are mostly simple)

* and with all this, implemented Enum and Class and Class[] Annotation elements, both on the JPF
(AnnotationInfo) and the modeling side. AnnotationInfo stores class elements as ClassInfo references,
and Enums as FieldInfo references (not sure if there could be other field refs in Annotations, but
assume not). This was quite a tour de force

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/jvm/ClinitRequired.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 564
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=564&view=rev
Author:   pcmehlitz
Date:     2007-09-13 19:19:39 -0700 (Thu, 13 Sep 2007)

Log Message:
-----------
a rather large set of reflection related fixes to make MethodTester run under JPF
among the more serious ones:

* Class.forName() didn't throw a ClassNotfoundException!! ..and nobody noticed this?

* of course we should only unbox box types in Method.invoke() if the argument type
is not a box type reference

* some missing methods in Contructor/Method

* the AnnotationProxy methods have to get the right operand and local slots

now it runs, including the Antlr parser. But the MemoryGoal needs a listener implementation
to not count the MethodTester itself

Modified Paths:
--------------
    trunk/env/jpf/java/lang/reflect/Constructor.java
    trunk/env/jpf/java/lang/reflect/Field.java
    trunk/env/jpf/java/lang/reflect/Method.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/test/MemoryGoal.java
    trunk/src/gov/nasa/jpf/test/TestContext.java
    trunk/src/gov/nasa/jpf/tools/MethodTester.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 569
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=569&view=rev
Author:   pcmehlitz
Date:     2007-09-17 11:51:35 -0700 (Mon, 17 Sep 2007)

Log Message:
-----------
* slightly extended the MJIEnv interface, adding add/removeListener() and getMethodInfo(ref)

* there was no JPF.removeListener - strange

* with that, implemented the precise ...test.MemoryGoal native peer as a listener. Well, almost precise,
because object heap size is of course VM specific. But the point is that we can keep track of
allocation/deallocation on a per-object basis. This should be good enough for an initial example
of how (and why) to do JPF specific goal implementations

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 571
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=571&view=rev
Author:   pcmehlitz
Date:     2007-09-17 17:56:04 -0700 (Mon, 17 Sep 2007)

Log Message:
-----------
* fixed pretty bad and subtle bug with Method/Contructor.getParameterTypes(), which is supposed to return
an array of class objects. However, if the classes are not initilialized yet, we have nulls in there.
So it needs a ClinitRequired exception from env.getParameterTypes(). But that just unveiled another bug
in env.handleClinitRequired() - no matter if we pushed clinit frames, we have to do a repeatInvocation() because
this is called from a handler context, and if we only had to create the class objects and hence go on,
we are in a gloriously inconsistent program state

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 573
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=573&view=rev
Author:   pcmehlitz
Date:     2007-09-21 14:17:48 -0700 (Fri, 21 Sep 2007)

Log Message:
-----------
* apparently forgot to update the MemoryGoal, JPF version

* core support for getting field/local values by name, and turning them
into Objects (required for the upcoming contracts). Required some refactoring
to get object sizes via polymorphism (pushed down into the FieldInfos)

* MJIEnv had a dependency on JPF_java_lang_reflect_Method, which is
of course illegal

* build.xml wasn't aware of the 'app' dir, which unfurtunately contains things
(Annotations) that are used by the core (the 'gov.nasa.jpf.test' stuff). But since
'app' is not allowed to use JPF specifics, I guess it's Ok to make the core
depend on it. Again, the purpose of 'app' is to use it for classes/interfaces/annotations
that can also be used by applications w/o JPF

Modified Paths:
--------------
    trunk/build.xml
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/DynamicElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.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/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/Types.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 577
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=577&view=rev
Author:   pcmehlitz
Date:     2007-09-24 17:31:45 -0700 (Mon, 24 Sep 2007)

Log Message:
-----------
* implementation for a simple contract grammar, including semantic actions to
construct a Contract object out of the specs

* the ContractVerifier is still a stub

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/Requires.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractAnd.java
    trunk/src/gov/nasa/jpf/test/ContractException.java
    trunk/src/gov/nasa/jpf/test/ContractOr.java
    trunk/src/gov/nasa/jpf/test/ContractSpec.g
    trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
    trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
    trunk/src/gov/nasa/jpf/test/SimpleContract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 578
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=578&view=rev
Author:   pcmehlitz
Date:     2007-09-24 20:27:38 -0700 (Mon, 24 Sep 2007)

Log Message:
-----------
* some more work on the ContractVerifier, which now parses and stores preconditions

* super contract handling. comes quite easy

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/EmptyContract.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.

Revision: 579
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=579&view=rev
Author:   pcmehlitz
Date:     2007-09-24 22:52:10 -0700 (Mon, 24 Sep 2007)

Log Message:
-----------
* couldn't help it - first stab at precond evaluation. Works, but has to be more
efficient, which also involves changing the syntax a bit to allow things like
"a within 0,42". The 'operand' rule needs to be widened, but that's why we
employ ANTLR

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractAnd.java
    trunk/src/gov/nasa/jpf/test/ContractOr.java
    trunk/src/gov/nasa/jpf/test/EmptyContract.java
    trunk/src/gov/nasa/jpf/test/SimpleContract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.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.

Revision: 580
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=580&view=rev
Author:   pcmehlitz
Date:     2007-09-25 15:07:07 -0700 (Tue, 25 Sep 2007)

Log Message:
-----------
* missed a bunch of box class constructors in MJIEnv

* likewise, primitive type field accessors in ElementInfo

* String.matches(regex) wasn't native? where did it go??

* fixed the Field.get(o) to do autoboxing and handle static fields

the FieldInfo tree needs to be extended to avoid these silly type.equals(..) checks. Not very OOPish

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 581
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=581&view=rev
Author:   pcmehlitz
Date:     2007-09-26 12:16:13 -0700 (Wed, 26 Sep 2007)

Log Message:
-----------
* hoisted SimpleContract.Operator and .Operand to toplevel - those are just getting bigger

* extended the grammar for operator/operand pairs to include more choices (like "within" and the generic
"satisfies"), though most of them don't have their eval implemented yet

* extended the functor to have any number of 'Operand' arguments

* added a cache for Operand.VarRef so that we don't have to lookup and create objects for
each occurrence in an expression. Actually, we might even need indentity at some point, so it's not just
an optimization 

* changed the precond evaluation to executeInstruction(), since we actually want to eval this
in the callers context (but need to check for performance)

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractSpec.g
    trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
    trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
    trunk/src/gov/nasa/jpf/test/SimpleContract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
    trunk/test/gov/nasa/jpf/test/TestContracts.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/Operand.java
    trunk/src/gov/nasa/jpf/test/Operator.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 585
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=585&view=rev
Author:   pcmehlitz
Date:     2007-09-28 10:39:35 -0700 (Fri, 28 Sep 2007)

Log Message:
-----------
* added some Verify.print() methods so that System.out clinits can be avoided if an
application really has to. Of course, you still have to use println(String...s) instead of 
String concatenation, to avoid the StringBuilder

* added some Verify.get/setFieldAttribute() methods, but those are mostly for debugging
attribute propagation w/o writing listeners. Only supports int attributes, since what would
it be good for trying to access native JPF objects from your application?

still need to do the corresponding array element attrs

* wrote a reg test case that shows how to use it

Modified Paths:
--------------
    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/jvm/TestAttrs.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 586
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=586&view=rev
Author:   pcmehlitz
Date:     2007-09-28 16:08:23 -0700 (Fri, 28 Sep 2007)

Log Message:
-----------
* added the array element attributes, which was mostly a little refactoring in
Fields/ArrayFields, plus the interface in ElementInfo

* added MJIEnv interfaces

* added all the stuff that potentially access elment attributes (System.arraycopy,
ArrayStore/LoadInstruction)

* fixed a bug with long GET/PUTFIELD ArrayLoad/StoreInstruction values, which of
course have to undergo the dreaded "attribute on first word" checks

* added test cases for it (using the Verify interface)

hopefully that is it

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
    trunk/src/gov/nasa/jpf/jvm/ArrayFields.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/Fields.java
    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/src/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 607
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=607&view=rev
Author:   ubnepvpb
Date:     2007-10-12 15:36:05 -0700 (Fri, 12 Oct 2007)

Log Message:
-----------
Doubles & Symbolic Execution:
- Add most of the double byte codes
- Fix INVOKExxx to work with doubles
- Add some test cases
- Add some JPF VMListeners to help with debugging

Modified Paths:
--------------
    trunk/.classpath
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FCMPL.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/bytecode/PC3WayChoiceGenerator.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/PCChoiceGenerator.java

Added Paths:
-----------
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DADD.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DCMPL.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DDIV.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DMUL.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DNEG.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DREM.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DSUB.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/Debug.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/LineNumberListener.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/PathConditionListener.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDouble1.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDoubleSpecial1.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDoubleVirtual1.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 634
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=634&view=rev
Author:   pcmehlitz
Date:     2007-10-18 13:43:48 -0700 (Thu, 18 Oct 2007)

Log Message:
-----------
* added optional event receiver constraints. For scripts, this is specified as

   [<receiver-pattern> {'|' <receiver-pattern> } ':'] <event-name> ['(' <args> ')']
   
where receiver pattern is using or StringSetMatcher notation, NOT general regexes, which means the only
meta char is the wildcard '*' (like a Unix wildcard char).

Explicitly sent events don't need receiver constraints, because they get them automatically. If we send an event to
an explicitly specified state, this implies it's only processed by itself or its children. Sounds sound, but the
implementation hurts (we pull it out of the PendingEvents queue of the receiver, just to encode the receiver again
in the SCEvent id). Nothing is perfect. At least, the receiver filter is consistent (all in NativeStateMachine and
SCEvent)

The SimStateMachine still needs to be updated accordingly

* added a little ReceiverConstraints example for this

* added a multiple-instances filter to NativeStateMachine.createCGFromPendingEvents(), since the hierarchical
lookup can lead to multiple inclusions of the same event, which just makes life harder for the model checker

Modified Paths:
--------------
    trunk/examples/jpfESAS/launch/CEV-ascent-guards.launch
    trunk/examples/jpfESAS/launch/CEV-safehold.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless-bt.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless-constraints.launch
    trunk/examples/jpfESAS/launch/CEV-scriptless.launch
    trunk/examples/jpfESAS/launch/CEV-tli.launch
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
    trunk/src/gov/nasa/jpf/util/StringSetMatcher.java

Added Paths:
-----------
    trunk/extensions/statechart/examples/ReceiverConstraints.es
    trunk/extensions/statechart/examples/ReceiverConstraints.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 638
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=638&view=rev
Author:   pcmehlitz
Date:     2007-10-18 17:49:57 -0700 (Thu, 18 Oct 2007)

Log Message:
-----------
* the missing SimStateMachine receiver constraint support

note that the explicit send support is not yet correct: sendEvent(a,"foo") should match a.foo() or a.whatever.foo(),
but not abc.foo(). But it seems this belongs to StringSetMatcher and can be fixed later (the regex just gets
a bit more complicated)

Modified Paths:
--------------
    trunk/examples/jpfESAS/launch/CEV-las-defect-sim.launch
    trunk/examples/jpfESAS/launch/CEV-nominal-sim.launch
    trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 642
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=642&view=rev
Author:   pcmehlitz
Date:     2007-10-22 14:10:28 -0700 (Mon, 22 Oct 2007)

Log Message:
-----------
* fixed the annoying JPFException when specifying a non-existing application class (actually, it handles all
startup classes the same way now)

* added a Verify.set/getLocalAttr() debug method

* had to slightly change StackFrame.getLocalOffset() handling for this, which shouldn't throw an
exception anyways

* simplified the TestAttrsNew, which is going to be removed now anyways

* fixed the "lost attribute on backtrack" bug, which was nothing else than just a Fields.equals() that
wasn't aware of attributes. That's why it was spurious - sometimes, spuriousness tells a story.

* added attributes to the Fields hashing too. Not strictly required (hashCode isn't guaranteed to be unique
anyways), but seems like a good idea for sym exec (the other ones would get slowed down though) 

Modified Paths:
--------------
    trunk/examples/launch/basic-racer.launch
    trunk/examples/launch/conc-1-RA.launch
    trunk/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
    trunk/src/gov/nasa/jpf/jvm/Fields.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/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/Verify.java
    trunk/src/gov/nasa/jpf/util/HashData.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrsNew.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 643
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=643&view=rev
Author:   pcmehlitz
Date:     2007-10-29 13:31:58 -0700 (Mon, 29 Oct 2007)

Log Message:
-----------
* added return value reflection in ReturnInstruction

* added general local/parameter value reflection to Instruction (that doesn't
make the InvokeInstruction.getArgumentValues() irrelevant though, since it works
on the StackFrame the insn belongs to)

* with that, implemented a first version of PostConditions, including "old" values

I don't like the separation between old/current values, and the (lack of)
encapsulation, so I might still refactor this a bit

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/StaticElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ARETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DRETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FRETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/IRETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LRETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/RETURN.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractAnd.java
    trunk/src/gov/nasa/jpf/test/ContractOr.java
    trunk/src/gov/nasa/jpf/test/EmptyContract.java
    trunk/src/gov/nasa/jpf/test/Operand.java
    trunk/src/gov/nasa/jpf/test/SimpleContract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.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.

Revision: 644
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=644&view=rev
Author:   pcmehlitz
Date:     2007-10-29 16:37:24 -0700 (Mon, 29 Oct 2007)

Log Message:
-----------
* forgot to commit @Ensures - Mea Culpa

* refactored and unified the value storage, which is now completely in ContractVerifier
(there was no need to have separate old and crrent value caches)

* refactored the error reporting, but I don't like it yet

* some fixes reg. handling of EmptyContract instances, esp. if the mdc contract
is empty. All the cotract hierarchy handling should be in class Contract itself

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractAnd.java
    trunk/src/gov/nasa/jpf/test/ContractOr.java
    trunk/src/gov/nasa/jpf/test/EmptyContract.java
    trunk/src/gov/nasa/jpf/test/Operand.java
    trunk/src/gov/nasa/jpf/test/SimpleContract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/Ensures.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 645
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=645&view=rev
Author:   pcmehlitz
Date:     2007-10-31 19:07:39 -0700 (Wed, 31 Oct 2007)

Log Message:
-----------
* refactored the contract evaluation to turn the variable lookup policy into an object
(the old rule still holds: "if in doubt, turn it into an object"). The policy root class
VarLookup is now responsible for the caching (incl. old values)

this looks better, except of the error reporting, which is still hacked

* with this, implemented instance invariants. Currently, it's only evaluating at
ReturnInstructions of instance methods, and only if it's not a ctor.

This should be extended to method entry, static invariants and ctors. A question
that still remains is what to do with base class methods - shall we eval the
invariant above the level where it is introduced? At least base ctors need to
be filtered out, since they can hardly satisfy invariants for fields that aren't
initialized yet.

this still needs some thinking, but the infrastructure is in place

also need to add a @StaticInvariant, and maybe rename @Invariant accordingly,
so that it becomes obvious which one is evaluated in what context

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractAnd.java
    trunk/src/gov/nasa/jpf/test/ContractOr.java
    trunk/src/gov/nasa/jpf/test/EmptyContract.java
    trunk/src/gov/nasa/jpf/test/Operand.java
    trunk/src/gov/nasa/jpf/test/SimpleContract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
    trunk/test/gov/nasa/jpf/test/TestContracts.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/Invariant.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 646
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=646&view=rev
Author:   pcmehlitz
Date:     2007-11-01 11:05:08 -0700 (Thu, 01 Nov 2007)

Log Message:
-----------
* Duhh - forgot to commit the VarLookup (explicit commit selection in Eclipse is error-prone)

* added null operands

* added a hook for special variables (e.g. computed by the VM)

* changed the var lookup so that it can also handle null values

* added a Operand.CenterInterval, but the value conversion is kind of braindead - should
probably implement a full set of numeric operations for Operands, or it gets really messy
in terms of ad hoc type conversions

Modified Paths:
--------------
    trunk/app/gov/nasa/jpf/Const.java
    trunk/app/gov/nasa/jpf/Ensures.java
    trunk/app/gov/nasa/jpf/Invariant.java
    trunk/app/gov/nasa/jpf/Requires.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/test/ContractSpec.g
    trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
    trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
    trunk/src/gov/nasa/jpf/test/Operand.java
    trunk/test/gov/nasa/jpf/test/TestContracts.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/StaticInvariant.java
    trunk/src/gov/nasa/jpf/test/VarLookup.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 647
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=647&view=rev
Author:   pcmehlitz
Date:     2007-11-01 22:06:33 -0700 (Thu, 01 Nov 2007)

Log Message:
-----------
* added support for "String[] value" annotations, which are instantiated as conjunctions of contracts.
Not sure if that should be the same for pre- and post-conditions, but we sure need it for @Invariants,
and there a conjunction seems the only natural choice

Modified Paths:
--------------
    trunk/.classpath
    trunk/app/gov/nasa/jpf/Invariant.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.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.

Revision: 648
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=648&view=rev
Author:   pcmehlitz
Date:     2007-11-05 19:09:49 -0800 (Mon, 05 Nov 2007)

Log Message:
-----------
* AASTORE should check array element type compatibility for non-null element values
Thanks Tihomir Gvero and Milos Gligoric

* added TestArray test case for ArrayStoreExceptions (and finally converted it into
a RawTest class)

Modified Paths:
--------------
    trunk/.classpath
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java
    trunk/test/gov/nasa/jpf/jvm/TestArray.java
    trunk/test/gov/nasa/jpf/jvm/TestArrayJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 649
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=649&view=rev
Author:   pcmehlitz
Date:     2007-11-06 15:13:06 -0800 (Tue, 06 Nov 2007)

Log Message:
-----------
* 'permit' field was not initialized for main thread. still needs some refactoring though

* added a little test for Martijn Hendriks example, but it's not in the regression suite yet
since I still have to verify the deadlock

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/jvm/TestCountDownLatch.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 650
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=650&view=rev
Author:   pcmehlitz
Date:     2007-11-07 12:30:12 -0800 (Wed, 07 Nov 2007)

Log Message:
-----------
* added Runtime.availableProcessors(), together with a little test case. All the data acquisition 
APIs in Runtime should be optionally turned into CGs (which is the case if "+cg.max_processors" is > 1)

* refactored the other API CG relevant settings to be under the "cg.*" section (enumerate_boolean, randomize_choices etc.)  

Modified Paths:
--------------
    trunk/default.properties
    trunk/env/jpf/java/lang/Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Runtime.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
    trunk/test/gov/nasa/jpf/jvm/TestThread.java
    trunk/test/gov/nasa/jpf/jvm/TestThreadJPF.java
    trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/jvm/TestRuntime.java
    trunk/test/gov/nasa/jpf/jvm/TestRuntimeJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 651
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=651&view=rev
Author:   pcmehlitz
Date:     2007-11-15 14:52:57 -0800 (Thu, 15 Nov 2007)

Log Message:
-----------
* streamlined the ClassInfo.isInstanceOf implementation - the "instanceOf(String)" and "isInstanceOf(ClassInfo)" actually
behaved differently (the latter one not checking for interface types). renamed it so that it consistently uses
isInstanceOf, the string version being the real implementation (so that we can test w/o forcing to load classfiles)

* changes CHECKCAST accordingly (the old normalized type name blues)

* added a few more tests to TestJavaLangClass and changed TestCast accordingly

now it passes the UI examples again (which were producing ArrayStoreExceptions because of interface type arrays, using isInstaceOf(ci) for element type compatibility checks)

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
    trunk/extensions/ui/env/jvm/gov/nasa/jpf/jvm/JPF_java_awt_EventDispatchThread.java
    trunk/extensions/ui/env/jvm/gov/nasa/jpf/jvm/JPF_java_awt_Window.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    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/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/Types.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/abstractor/FilterBasedAbstractorConfiguration.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
    trunk/src/gov/nasa/jpf/jvm/choice/TypedObjectChoice.java
    trunk/test/gov/nasa/jpf/jvm/TestCast.java
    trunk/test/gov/nasa/jpf/jvm/TestCastJPF.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 652
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=652&view=rev
Author:   pcmehlitz
Date:     2007-11-19 22:14:18 -0800 (Mon, 19 Nov 2007)

Log Message:
-----------
* some more System.arraycopy element type checks (reference element types - thanks to Milos Gligoric and Tihomir Gvero,
ref/builtin, builtin/builtin, both single- and double word)

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
    trunk/test/gov/nasa/jpf/jvm/TestArray.java
    trunk/test/gov/nasa/jpf/jvm/TestArrayJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 666
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=666&view=rev
Author:   pcmehlitz
Date:     2007-11-27 20:23:02 -0800 (Tue, 27 Nov 2007)

Log Message:
-----------
* Java SE 6 unveiled a forgotten check in the CHECKCAST insn - thanks to Franck van Breugel

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
    trunk/test/gov/nasa/jpf/jvm/TestCast.java
    trunk/test/gov/nasa/jpf/jvm/TestCastJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 671
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=671&view=rev
Author:   pcmehlitz
Date:     2007-11-29 11:32:54 -0800 (Thu, 29 Nov 2007)

Log Message:
-----------
* revamped contract grammar and interpreter - still a long way to go (array subscripts, functions, exception contracts,
open/closed intervals, sets, ...), but at least that's a better basis now. The big thing is that we have expressions
over operand values, including a generic "old(<expr>)" (so that we can store arbitrary exprs pre-exec)

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractAnd.java
    trunk/src/gov/nasa/jpf/test/ContractOr.java
    trunk/src/gov/nasa/jpf/test/ContractSpec.g
    trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
    trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
    trunk/src/gov/nasa/jpf/test/EmptyContract.java
    trunk/src/gov/nasa/jpf/test/Operand.java
    trunk/src/gov/nasa/jpf/test/VarLookup.java
    trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
    trunk/test/gov/nasa/jpf/test/TestContracts.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/Expr.java

Removed Paths:
-------------
    trunk/src/gov/nasa/jpf/test/SimpleContract.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 672
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=672&view=rev
Author:   pcmehlitz
Date:     2007-11-29 12:12:05 -0800 (Thu, 29 Nov 2007)

Log Message:
-----------
* @UntrackedField extension from Tihomir Gvero and Milos Gligoric.

This is a general solution for the problem of
accumulating values over all paths (i.e. vars that don't get restored upon backtrack), and e.g. comes in handy for
test applications (= JPF specific models) that do some kind of coverage analysis. Be aware of the 'Heisenberg' in
there, but it's much better than the crude MJI based counters we used for testing so far, or any ad-hoc application
solutions. If you want the details, there is a Untracked.html in the docs

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/DynamicFields.java
    trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
    trunk/src/gov/nasa/jpf/jvm/Fields.java
    trunk/src/gov/nasa/jpf/jvm/StaticFields.java

Added Paths:
-----------
    trunk/doc/Untracked.html
    trunk/src/gov/nasa/jpf/jvm/untracked/
    trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedField.java
    trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedManager.java
    trunk/test/gov/nasa/jpf/mc/TestUntrackedField.java
    trunk/test/gov/nasa/jpf/mc/TestUntrackedFieldJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 689
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=689&view=rev
Author:   pcmehlitz
Date:     2007-12-05 22:37:20 -0800 (Wed, 05 Dec 2007)

Log Message:
-----------
* support for user defined state class hierarchies, including masked state fields. Not sure
if that ever would make sense from a modeling standpoint (to the contrary - I am sure it doesn't),
but with some extra effort (explicitly walking the class hierarchy) we can also initialize the
masked fields. Seems worth it to prevent some very strange runtime behaviors that ultimately run into
uninitialized state objects with names of initialized ones. very confusing!

Modified Paths:
--------------
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_State.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.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.

Revision: 697
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=697&view=rev
Author:   pcmehlitz
Date:     2007-12-11 11:37:07 -0800 (Tue, 11 Dec 2007)

Log Message:
-----------
* Tihomir's patch for long/double/short/byte/char annotation element types

* first stab at the SequenceAnalyzer, which is supposed to become an XMI exporter for UML sequence diagrams, produced from
running annotated Java programs. Still needs a long way to go though. It finally is (user) Trace<E> client. Actually, it even maintains two traces, but only one of them is a conceptual one (sequenceOps), the other one just abuses Trace to implement backtracking of the sequence context 

Modified Paths:
--------------
    trunk/env/jpf/java/lang/System.java
    trunk/env/jpf/java/lang/Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
    trunk/src/gov/nasa/jpf/util/Trace.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/NonNull.java
    trunk/app/gov/nasa/jpf/Sequence.java
    trunk/app/gov/nasa/jpf/SequenceEvent.java
    trunk/app/gov/nasa/jpf/SequenceObject.java
    trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotation.java
    trunk/test/gov/nasa/jpf/mc/TestAnnotationJPF.java
    trunk/test/gov/nasa/jpf/test/TestSequence.java

Removed Paths:
-------------
    trunk/src/gov/nasa/jpf/test/Operator.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 698
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=698&view=rev
Author:   pcmehlitz
Date:     2007-12-12 11:14:55 -0800 (Wed, 12 Dec 2007)

Log Message:
-----------
* rather embarrassing bug in ClassInfo.getAllInterfaces(), which was not working recursively up the inheritance chain. The recursion at some point was in loadInterfacesRecursively, but vanished. Bug report thanks to Louise Dennis

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/test/gov/nasa/jpf/jvm/TestCast.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 703
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=703&view=rev
Author:   pcmehlitz
Date:     2007-12-13 16:29:24 -0800 (Thu, 13 Dec 2007)

Log Message:
-----------
* next round for the SequenceAnalyzer. Added a SequenceProcessor abstraction to facilitate checks/reports on traces.
Added a default processor which writes out sequences in a format that's compatible to Alex Moffat's SEQUENCE
generator. Still needs a lot of cleanup and completion, and esp. a workaround for a BCEL bug that silently drops
annotation elements if there are default values

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
    trunk/src/gov/nasa/jpf/util/Trace.java
    trunk/test/gov/nasa/jpf/test/TestSequence.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/SequenceMethod.java
    trunk/src/gov/nasa/jpf/test/SequenceOp.java
    trunk/src/gov/nasa/jpf/test/SequenceProcessor.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 704
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=704&view=rev
Author:   pcmehlitz
Date:     2007-12-13 21:17:08 -0800 (Thu, 13 Dec 2007)

Log Message:
-----------
* added PUTFIELD init of object references and symbolic result names

Modified Paths:
--------------
    trunk/app/gov/nasa/jpf/SequenceMethod.java
    trunk/app/gov/nasa/jpf/SequenceObject.java
    trunk/src/gov/nasa/jpf/test/SequenceOp.java
    trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
    trunk/test/gov/nasa/jpf/test/TestSequence.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 708
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=708&view=rev
Author:   pcmehlitz
Date:     2007-12-14 20:49:11 -0800 (Fri, 14 Dec 2007)

Log Message:
-----------
* beginnings of @Requirement annotation extension for CoverageAnalyzer. It only stores the related MethodCoevarge
objects so far, statistics still need to be done

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
    trunk/src/gov/nasa/jpf/util/Misc.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/Requirement.java
    trunk/test/gov/nasa/jpf/test/TestRequirementsCoverage.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 710
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=710&view=rev
Author:   pcmehlitz
Date:     2007-12-16 22:27:48 -0800 (Sun, 16 Dec 2007)

Log Message:
-----------
* changed requirements coverage report so that it shows the complete set of requirements (from the class set), and
hence reports the requirements/method coverage correctly (i.e. including the non-loaded requirements methods). The insn,
BB and branch coverage is only reported for the loaded ones, which might be a bit misleading.

That of course makes it even more important to NOT use ClassInfos for getting all defined requirements methods from the
class set

* minor bug in Instruction.isCompleted(ti) - has to include terminated threads (we mainly get this from the thread stack)

* first round against the ConstChecker, a little listener that monitors @Const attributes. The static method @Const is still a joke (inefficient), and we really need to use memory pools for this. The "return clone on mod" pattern for the pseudo-traces
(which are really just backtrackable/restorable stacks) is Ok, but error prone. There needs to be better infrastructure for
listener specific state extensions

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
    trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
    trunk/test/gov/nasa/jpf/test/TestRequirementsCoverage.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/tools/ConstChecker.java
    trunk/test/gov/nasa/jpf/test/TestConst.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 711
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=711&view=rev
Author:   pcmehlitz
Date:     2007-12-16 22:43:39 -0800 (Sun, 16 Dec 2007)

Log Message:
-----------
* bug fix for casting builtin type arrays, thanks to Tihomir Gvero

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/test/gov/nasa/jpf/jvm/TestCast.java
    trunk/test/gov/nasa/jpf/jvm/TestCastJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 714
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=714&view=rev
Author:   pcmehlitz
Date:     2007-12-17 19:05:53 -0800 (Mon, 17 Dec 2007)

Log Message:
-----------
 * apparently, the non-ASCII +- char for center-interval tests screwed up either BCEL or ANTLR or both. Modified the
 grammar, the test, and the contract class to replace it with "+-"

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractSpec.g
    trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
    trunk/src/gov/nasa/jpf/test/ContractSpecParser.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.

Revision: 719
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=719&view=rev
Author:   pcmehlitz
Date:     2007-12-20 16:37:04 -0800 (Thu, 20 Dec 2007)

Log Message:
-----------
* changed @Requirement annotation to have a String array attribute, so that a method can be associated with several
requirements. Still needs some more polishing for the report (we probably should report the uncovered/not-loaded methods for each requirement). It's also worth it to extend the MethodTester to execute test exprs for certain requirements (not the whole class)

* added the Eclipse launch configs to the test dir

Modified Paths:
--------------
    trunk/app/gov/nasa/jpf/Requirement.java
    trunk/doc/JPF_files/JPF-mod.css
    trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
    trunk/test/gov/nasa/jpf/test/TestMethodTest.java
    trunk/test/gov/nasa/jpf/test/TestRequirementsCoverage.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/test/TestConst.launch
    trunk/test/gov/nasa/jpf/test/TestContracts.launch
    trunk/test/gov/nasa/jpf/test/TestMethods-standalone.launch
    trunk/test/gov/nasa/jpf/test/TestMethods.launch
    trunk/test/gov/nasa/jpf/test/TestRequirements.launch
    trunk/test/gov/nasa/jpf/test/TestSequence.launch


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 720
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=720&view=rev
Author:   pcmehlitz
Date:     2007-12-26 23:15:39 -0800 (Wed, 26 Dec 2007)

Log Message:
-----------
* bag of bug fixes from Tihomir & Darko

 - ConsoleOutputStream printf/format (w/o test, since only side effect)
 - Enum<T>.valueOf() fix (requires - package private - Class.enumConstantDirectory(), which uses a private Class field)
 - Class.getInterfaces() (according to doc, it was returning all interfaces, but it turns out that in reality it
 only should return the declared (direct) interfaces)
 - cloning of primitive type arrays
 
 The last one was the biggest change with quite some fan out - the real problem is yet again in the various different
 naming schemes (type code, dot/builtin, L-dot, L-slash). DynamicArea.newArray() tried to be too smart, which ended up in an
 ambiguity between builtin typecodes and user defined classes in the default package (e.g. "B"). Of course, we can
 only test this if we also allow rawtest/JPF driver combos in a test/ default package (Java >1.4 doesn't allow
 importing def package classes into named packages), which also required build.xml to be modified.
 
 NOTE - DynmaicArea.newArray() now expects L-slash notation! If you use the MJIEnv.newObjectArray() facade, you can still use
 normal dot names, but otherwise the burden is on the caller. THIS MIGHT BREAK SOME CODE OUT THERE
 
 A pity we hav to go through all this for the stupid case somebody wants to name default package classes "B", "C" etc.
 (which is unfortunately what everybody does with quick tests)
 
 * Fields.equals() had a bug with attribute comparison (missing branches) - thanks Hank
   

Modified Paths:
--------------
    trunk/build.xml
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_ConsoleOutputStream.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_State.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
    trunk/src/gov/nasa/jpf/jvm/Fields.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java

Added Paths:
-----------
    trunk/test/TestJavaLangObject.java
    trunk/test/TestJavaLangObjectJPF.java
    trunk/test/gov/nasa/jpf/jvm/TestEnum.java
    trunk/test/gov/nasa/jpf/jvm/TestEnumJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 721
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=721&view=rev
Author:   pcmehlitz
Date:     2007-12-27 11:16:30 -0800 (Thu, 27 Dec 2007)

Log Message:
-----------
* bag of patches from Jerry James - thanks!

 - compiler warnings about deprecated method calls
 - C compiler warnings for the native constraint solver interface code in extensions/symbolic/csrc
 - javadoc hickup fixes (not that we really have javadoc docu - mea culpa)
 - a LOT of StringBuffer/Builder cleanups (use StringBuilder, use explicit init, avoid
 single-char strings etc.). Mostly minor performance optimizations, but there's no excuse of being sloppy. Now if only
 somebody would step in and provide similar patches for replacing Debug (with our logging) and other ever-pending
 cleanups
 
 There seems to be a problem with older Solaris javac's when compiling Thread.exit(), but the
 suggested fix would break Java SE6. However, that just brings up the issue of reinstating
 Thread.exit(), which is next

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Thread.java
    trunk/examples/ase2006/Crossing.java
    trunk/examples/ase2006/CrossingListener.java
    trunk/examples/ase2006/CrossingNative.java
    trunk/examples/jpfESAS/launch/CV-generate-assumption-1.launch
    trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/Attributes.java
    trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/Edge.java
    trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/Generate.java
    trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/SM2Dot.java
    trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/trans/Formula.java
    trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/trans/Transition.java
    trunk/extensions/cv/src/gov/nasa/jpf/cv/SETLearner.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/symbolic/csrc/cvcl-inc.c
    trunk/extensions/symbolic/csrc/cvcl-incsolve.c
    trunk/extensions/symbolic/csrc/cvcl.c
    trunk/extensions/symbolic/csrc/yices-inc.c
    trunk/extensions/symbolic/csrc/yices-incsolve.c
    trunk/extensions/symbolic/csrc/yices.c
    trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/dp/CVCLInterface.java
    trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/dp/OmegaInterface.java
    trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/ConstraintBuilder.java
    trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/JPF_gov_nasa_jpf_symbolic_integer_SymbolicConstraints.java
    trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/Reconstruction.java
    trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIAction.java
    trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
    trunk/src/gov/nasa/jpf/Config.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/ArrayFields.java
    trunk/src/gov/nasa/jpf/jvm/BooleanChoiceGenerator.java
    trunk/src/gov/nasa/jpf/jvm/ChoiceGenerator.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DynamicArea.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/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/SingleFieldLockInfo.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/StatisticFieldLockInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadData.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/Types.java
    trunk/src/gov/nasa/jpf/jvm/Verify.java
    trunk/src/gov/nasa/jpf/jvm/choice/CustomBooleanChoiceGenerator.java
    trunk/src/gov/nasa/jpf/jvm/choice/DoubleThresholdGenerator.java
    trunk/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java
    trunk/src/gov/nasa/jpf/jvm/choice/IntIntervalGenerator.java
    trunk/src/gov/nasa/jpf/jvm/choice/IntSpec.java
    trunk/src/gov/nasa/jpf/jvm/choice/InvocationCG.java
    trunk/src/gov/nasa/jpf/tools/GenPeer.java
    trunk/src/gov/nasa/jpf/tools/GenPeerDispatcher.java
    trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
    trunk/src/gov/nasa/jpf/tools/StateSpaceDot.java
    trunk/src/gov/nasa/jpf/util/Debug.java
    trunk/src/gov/nasa/jpf/util/DynamicIntArray.java
    trunk/src/gov/nasa/jpf/util/DynamicObjectArray.java
    trunk/src/gov/nasa/jpf/util/Inspector.java
    trunk/src/gov/nasa/jpf/util/JPFRunner.java
    trunk/src/gov/nasa/jpf/util/Printable.java
    trunk/src/gov/nasa/jpf/util/script/Event.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 722
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=722&view=rev
Author:   pcmehlitz
Date:     2008-01-02 12:12:41 -0800 (Wed, 02 Jan 2008)

Log Message:
-----------
* finally took the time and fixed the annoying triple reporting of JPF internal exceptions

* also finally did proper adding/removal of threads to ThreadGroups, including the main thread. This came together
with some reworking of thread termination processing. In the standard libs, this is done by magically calling
a Thread.exit(), which then calls ThreadGroup.remove(t), but this involves locking and notification from the
global (shared) ThreadGroup object, and the last thing we want is additional states when we are done with the app.
So we forego a bit of fidelity in favor of readability/efficiency. Also updated the TestThread accordingly

* the cyclic reference between Thread<->ThreadGroup unveiled a bug in UntrackedManager, which was fixed temporarily 
but needs to be revisited for performance reasons


with this out of the way, next in the list of open threading issues is to reinstate Verify.begin/endAtomic() the right way (if you really need it)

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
    trunk/src/gov/nasa/jpf/JPFException.java
    trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/PrioritySchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/SchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadList.java
    trunk/src/gov/nasa/jpf/jvm/abstraction/abstractor/AbstractorBasedBuilder.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/jvm/bytecode/ReturnInstruction.java
    trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedManager.java
    trunk/test/gov/nasa/jpf/jvm/TestThread.java
    trunk/test/gov/nasa/jpf/jvm/TestThreadJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 723
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=723&view=rev
Author:   pcmehlitz
Date:     2008-01-03 15:57:24 -0800 (Thu, 03 Jan 2008)

Log Message:
-----------
* the die-hard Verify.begin/endAtomic() is back! It's a different animal though - it works by short-cutting
the CG creation in the SchedulerFactory instances, and tolerates data CGs inside of atomic sections. It still
does not allow blocking inside an atomic section, but other than the old version reports this as a
deadlock, i.e. property violation, and not a silly JPF internal error (which it isn't - it's an
application problem).

* this required some reshuffle of the deadlock detection, which now mostly resides in ThreadList

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.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/KernelState.java
    trunk/src/gov/nasa/jpf/jvm/PrioritySchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/SystemState.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/ThreadList.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
    trunk/test/gov/nasa/jpf/mc/TestAtomic.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/mc/TestAtomicJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 726
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=726&view=rev
Author:   pcmehlitz
Date:     2008-01-08 17:31:08 -0800 (Tue, 08 Jan 2008)

Log Message:
-----------
* refactoring of DCMPx, FCMPx, LCMP to better suit subclassing for the symbc extension - thanks to Adam Kiezun

* replaced the somewhat braindead clone() of the StackFrame hierarchy with a covariant version that's based on
the generic one. Removes a couple of superfluous casts, but more importantly removes the need for clone()
overriding in DirectCallStackFrame.

>> I'm sure there are a gazillion of other screwed clones that wait to be
cleaned up, so somebody could earn immortal fame doing this

* extended the InfoObject interface with a getClassInfo(), so that the aggregate type can be queried (returns
itself for ClassInfos)

* some work on the generic Contract.Satisfies, but it's NOT yet really working - the Predicate interface
needs to be based on Operand. Introduced a ContractContext (analogous to the slightly outdated TestContext)
for the purpose of explicit conversion (it's the dreaded ElementInfo -> Java object), but it's not complete yet.
At least that also solve the class resolution problem for Predicate classes (default - package of contract specifier)

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/DirectCallStackFrame.java
    trunk/src/gov/nasa/jpf/jvm/InfoObject.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/SystemState.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DCMPG.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/DCMPL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FCMPG.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/FCMPL.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/LCMP.java
    trunk/src/gov/nasa/jpf/report/Reporter.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractSpec.g
    trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
    trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
    trunk/test/gov/nasa/jpf/test/TestContracts.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/test/ContractContext.java
    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.

Revision: 734
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=734&view=rev
Author:   pcmehlitz
Date:     2008-01-22 14:58:47 -0800 (Tue, 22 Jan 2008)

Log Message:
-----------
* somehow, the attribute hashing for StackFrames got lost, and out of sync with Fields hashing. Now
it's in for both, but maybe we should turn it into an option

* SimpleDateFormat was missing a non-public method that is used from its DateFormat factory. The workaround
is kind of suboptimal, since we use the factory on the native side to indirectly create an equivalent
native DateFormat (since we can't call the package default method), but of course that is making
assumptions about library code we don't see

Modified Paths:
--------------
    trunk/env/jpf/java/text/SimpleDateFormat.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
    trunk/src/gov/nasa/jpf/jvm/Fields.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

Revision: 735
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=735&view=rev
Author:   pcmehlitz
Date:     2008-01-25 10:47:30 -0800 (Fri, 25 Jan 2008)

Log Message:
-----------
* forgotten metrics builder reference in Eclipse .project file

* somehow the jpfESAS/doc dir got lost. Reinstated, but needs to be cleaned up

* bug in thread termination - we have to check if we can acquire the thread object lock for
post mortem notification, otherwise we can run into a locking assertion. For
consistency reasons moved the notification from ThreadInfo.finish() over to ReturnInstruction.execute
(better keep everything together). Used a MonitorEnterCG for blocking, which is slightly
suspicious since there is no corresponding MonitorExitCG, but should only matter if we
have SchedulerFactories that rely on symmetry (the monitor_exit is usually a left mover for
us anyways) 

Modified Paths:
--------------
    trunk/.project
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java

Added Paths:
-----------
    trunk/examples/jpfESAS/doc/
    trunk/examples/jpfESAS/doc/Ascent-ambiguity.graffle
    trunk/examples/jpfESAS/doc/Ascent-ambiguity.png
    trunk/examples/jpfESAS/doc/Ascent-las.graffle
    trunk/examples/jpfESAS/doc/Ascent-las.png
    trunk/examples/jpfESAS/doc/Ascent.graffle
    trunk/examples/jpfESAS/doc/Ascent.png
    trunk/examples/jpfESAS/doc/CEV-example.html
    trunk/examples/jpfESAS/doc/CEV_15EOR_LOR-DRM.png
    trunk/examples/jpfESAS/doc/CEV_15EOR_LOR-model.png
    trunk/examples/jpfESAS/doc/CEV_15EOR_LOR.graffle
    trunk/examples/jpfESAS/doc/CEV_15EOR_LOR.png
    trunk/examples/jpfESAS/doc/EarthOrbit-safehold.graffle
    trunk/examples/jpfESAS/doc/EarthOrbit-safehold.png
    trunk/examples/jpfESAS/doc/EarthOrbit-tli.graffle
    trunk/examples/jpfESAS/doc/EarthOrbit-tli.png
    trunk/examples/jpfESAS/doc/EarthOrbit.graffle
    trunk/examples/jpfESAS/doc/EarthOrbit.png
    trunk/examples/jpfESAS/doc/Entry.graffle
    trunk/examples/jpfESAS/doc/Entry.png
    trunk/examples/jpfESAS/doc/LunarOps.graffle
    trunk/examples/jpfESAS/doc/LunarOps.png
    trunk/examples/jpfESAS/doc/Transit.graffle
    trunk/examples/jpfESAS/doc/cv.html
    trunk/examples/jpfESAS/doc/demo-script.html
    trunk/examples/jpfESAS/doc/doc.css
    trunk/examples/jpfESAS/doc/executable-models.html
    trunk/examples/jpfESAS/doc/jpf-statecharts.html
    trunk/examples/jpfESAS/doc/model.html
    trunk/examples/jpfESAS/doc/toolchain.graffle
    trunk/examples/jpfESAS/doc/toolchain.png
    trunk/examples/jpfESAS/doc/uml.html


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.