Thread: [Javapathfinder-devel] SF.net SVN: javapathfinder: [474] trunk (Page 4)

Status: Beta

Brought to you by: artimid, johnpenix, masoud_mansouri, pcdillinger, and 3 others

javapathfinder-devel

[Javapathfinder-devel] SF.net SVN: javapathfinder: [474] trunk

From: <pcm...@us...> - 2007-08-03 20:59:26

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [478] trunk

From: <pcm...@us...> - 2007-08-06 19:22:49

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [499] trunk

From: <pcm...@us...> - 2007-08-09 06:02:41

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [509] trunk

From: <pcm...@us...> - 2007-08-10 23:04:59

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [511] trunk

From: <pcm...@us...> - 2007-08-13 21:25:21

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [512] trunk

From: <pcm...@us...> - 2007-08-14 05:07:23

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [514] trunk

From: <pcm...@us...> - 2007-08-14 23:36:55

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [515] trunk

From: <pcm...@us...> - 2007-08-16 01:02:59

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [516] trunk

From: <pcm...@us...> - 2007-08-16 17:45:02

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [517] trunk

From: <pcm...@us...> - 2007-08-17 00:31:15

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [518] trunk

From: <pcm...@us...> - 2007-08-17 20:17:08

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [520] trunk

From: <pcm...@us...> - 2007-08-18 19:29:04

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [521] trunk

From: <pcm...@us...> - 2007-08-21 01:28:59

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [523] trunk

From: <pcm...@us...> - 2007-08-23 07:25:43

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [531] trunk

From: <pcm...@us...> - 2007-08-24 05:42:32

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [535] trunk

From: <pcm...@us...> - 2007-08-24 23:02:56

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [536] trunk

From: <pcm...@us...> - 2007-08-24 23:41:18

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [538] trunk

From: <pcm...@us...> - 2007-08-30 06:26:46

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [540] trunk

From: <pcm...@us...> - 2007-08-31 05:30:10

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [541] trunk

From: <pcm...@us...> - 2007-09-02 04:03:10

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [542] trunk

From: <pcm...@us...> - 2007-09-03 09:47:05

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [545] trunk

From: <pcm...@us...> - 2007-09-05 00:21:09

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [546] trunk

From: <pcm...@us...> - 2007-09-05 19:29:01

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [547] trunk

From: <pcm...@us...> - 2007-09-05 23:32:32

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.

[Javapathfinder-devel] SF.net SVN: javapathfinder: [549] trunk

From: <pcm...@us...> - 2007-09-06 18:25:00

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.

<< < 1 2 3 4 5 6 7 > >> (Page 4 of 7)