Menu
▾
▴
javapathfinder-devel — development related topics (your place if you work with the sources)
You can subscribe to this list here.
| 2005 |
Jan
|
Feb
|
Mar
|
Apr
(9) |
May
(38) |
Jun
(13) |
Jul
(3) |
Aug
(14) |
Sep
(25) |
Oct
(44) |
Nov
(6) |
Dec
(2) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2006 |
Jan
(4) |
Feb
(14) |
Mar
(16) |
Apr
(2) |
May
(1) |
Jun
(2) |
Jul
(2) |
Aug
(1) |
Sep
(1) |
Oct
|
Nov
(3) |
Dec
(1) |
| 2007 |
Jan
(3) |
Feb
(39) |
Mar
(30) |
Apr
(31) |
May
(20) |
Jun
(72) |
Jul
(41) |
Aug
(78) |
Sep
(48) |
Oct
(59) |
Nov
(31) |
Dec
(47) |
| 2008 |
Jan
(18) |
Feb
(37) |
Mar
(45) |
Apr
(78) |
May
(16) |
Jun
|
Jul
(8) |
Aug
(10) |
Sep
(23) |
Oct
(10) |
Nov
(12) |
Dec
(1) |
| 2009 |
Jan
(4) |
Feb
|
Mar
(3) |
Apr
(1) |
May
(1) |
Jun
(1) |
Jul
|
Aug
|
Sep
(1) |
Oct
(3) |
Nov
(2) |
Dec
|
| 2010 |
Jan
(1) |
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2013 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(2) |
Oct
|
Nov
|
Dec
|
|
From: <pcm...@us...> - 2008-02-20 00:33:36
|
Revision: 748
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=748&view=rev
Author: pcmehlitz
Date: 2008-02-19 16:33:33 -0800 (Tue, 19 Feb 2008)
Log Message:
-----------
* workaround for some quirky KC hack that unconditionally removed sent events. In a KC environment, the only events
processed are from the pendingEvents queue, but not otherwise. Hence, we have to keep a list of events we have
to cleanup in the bottom half of NativeStateMachine.getPendingEvents() (we can't do this in the top half, because
then we might get state matched prematurely). The good thing is we can keep this list on the native side, but we
have to add some info (EventSource) to SCEvent. The current EventSource?PendingEventSource stuff is a bit
over-engineered though
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
Added Paths:
-----------
trunk/extensions/statechart/examples/CompletionSend.es
trunk/extensions/statechart/examples/CompletionSend.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-19 23:24:07
|
Revision: 747
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=747&view=rev
Author: pcmehlitz
Date: 2008-02-19 15:24:04 -0800 (Tue, 19 Feb 2008)
Log Message:
-----------
* field attr update has to be consistent between PUTFIELD/PUTSTATIC. It also seems more natural to
'set' this unconditionally (i.e. the operand attr always is used to update the field attr - even if
it's null). If we ever want to do a conditional accumulation policy, this has to happen from within
the called method in ElementInfo
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-18 21:17:34
|
Revision: 746
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=746&view=rev
Author: pcmehlitz
Date: 2008-02-18 13:17:32 -0800 (Mon, 18 Feb 2008)
Log Message:
-----------
* forgot the ArrayFields in the DefaultFieldsFactory - thanks Tihomir
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DefaultFieldsFactory.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/FieldsFactory.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-15 06:01:09
|
Revision: 745
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=745&view=rev
Author: pcmehlitz
Date: 2008-02-14 22:01:07 -0800 (Thu, 14 Feb 2008)
Log Message:
-----------
* added an abstract factory to create Fields instances, which is a precursor for a customized object storage
model. We don't have that yet, but this also enables logging *all* field manipulations (incl. attributes), which
also comes in handy for the upcoming "undo" mode. What is not so nice is that we have to pass in a usually
not used reference to the ElementInfo holding the fields, which in turn required changing the default field init
(from consts). This now requires explicit initialization calls from Dynamic/StaticArea, whereas before it was
just part of the Fields creation.
With this, UntrackedManager references should be removed from the default Fields impl
The FieldsFactory class can be set with the 'vm.fields_factory.class' property, which was added to default.properties
Modified Paths:
--------------
trunk/.classpath
trunk/default.properties
trunk/examples/jpfESAS/launch/CV-assumption-1.launch
trunk/examples/launch/conc-2-RA_da.launch
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/DynamicElementInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicFields.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/FloatFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/IntegerFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/LongFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/StaticArea.java
trunk/src/gov/nasa/jpf/jvm/StaticElementInfo.java
trunk/src/gov/nasa/jpf/jvm/StaticFields.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedManager.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/jvm/DefaultFieldsFactory.java
trunk/src/gov/nasa/jpf/jvm/FieldsFactory.java
Removed Paths:
-------------
trunk/examples/jpfESAS/launch/CEV-las-defect.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-08 02:07:14
|
Revision: 744
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=744&view=rev
Author: pcmehlitz
Date: 2008-02-07 18:07:07 -0800 (Thu, 07 Feb 2008)
Log Message:
-----------
* added a more intuitive State.terminate(), which is synonym to State.setEndState(<masterState>), to terminate
the whole execution. Be aware this still processes all exitActions of the issuing state up to the masterState
* fixed a bug in StateMachine.step(), which caused the masterState to be erroneously added to the nextActives set
in case somebody globally terminates
* changed State.getName() to return the typeName if there is no fieldName, which is more readable if somebody
does things with the masterState (which doesn't have a fieldName)
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/examples/Ortho1.java
trunk/extensions/statechart/examples/Repeater.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
trunk/src/gov/nasa/jpf/util/script/EventGeneratorFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-06 22:13:37
|
Revision: 743
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=743&view=rev
Author: pcmehlitz
Date: 2008-02-06 14:13:19 -0800 (Wed, 06 Feb 2008)
Log Message:
-----------
* added partial wildcard ANYs to scripts, so you can do a
ANY { foo, bar, *baz }
which still causes alphabet expansion (to get all trigger methods of all active states via reflection), but then filters
by matching all found trigger names against the ANY patterns. This is actually more straight than the previous
ANY { * }, which is really just a special case
* added some 'hasAnyPattern' optimization to StringSetMatcher - no need to burn a lot of cycles on regex matching
if we know there is a "matches anything" pattern
* first stab on unbounded REPEATs, but there are subtle search termination issues remaining. This introduces
'instructions' (pseudo CGs) into the EventGeneratorFactory queue, which works Ok but should be refactored so that
we don't have to call the Jump a ChoiceGenerator. What doesn't work so well is that it creates infinite loops
if we never run out of active states (e.g. if triggers do not fire a transition). This is because with unconditional
Jumps we never run out of fresh CGs (the next CG is always reset in EventGeneratorFactory.getNextChoiceGenerator()). The
JVM nicely recognizes if it has visited a program state, but of course always goes on if the next CG says it still
has choices (because it was reset). So we need to make the Jump conditional, i.e. give it it's own state.
Once this is done, it should be used as the sole mechanism for REPEATs, and we should ditch the unrolling
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/examples/Repeater.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventFromSet.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGenerator.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventSingleChoice.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/util/StringSetMatcher.java
trunk/src/gov/nasa/jpf/util/script/ESParser.java
trunk/src/gov/nasa/jpf/util/script/EventGeneratorFactory.java
Added Paths:
-----------
trunk/extensions/statechart/examples/Wildcards.es
trunk/extensions/statechart/examples/Wildcards.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-05 23:04:22
|
Revision: 742
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=742&view=rev
Author: pcmehlitz
Date: 2008-02-05 15:04:14 -0800 (Tue, 05 Feb 2008)
Log Message:
-----------
* some left over doc updates
* empty event scripts caused parse exception, which they shouldn't
* revisited the unbounded REPEATs, but this is not functional yet. Needs to add a pseudo CG in EventGeneratorFactory,
which is used only to position in the CG queue. This would be some sort of a script insn, which we hadn't so far. Just
used simple unrolling to keep the backtracking simple, but of course that doesn't work with unbounded REPEATs
Modified Paths:
--------------
trunk/doc/JPF_files/JPF-mod.css
trunk/doc/home.html
trunk/doc/news.html
trunk/extensions/symbc/doc/index.html
trunk/src/gov/nasa/jpf/util/script/ESParser.java
Added Paths:
-----------
trunk/extensions/statechart/examples/Repeat.es
trunk/extensions/statechart/examples/Repeater.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: Peter C. M. <Pet...@na...> - 2008-02-05 02:24:37
|
Better late than never - we will have a two days workshop on 05/01 and 05/02 at the Fujitsu campus in Sunnyvale, CA. Tentative plans are to have "what is being done with JPF" presentations the first day, and reserve the second day for general and project specific JPF questions, BoF's and whatever might come up. Please have a look at the event web page <http:// javapathfinder.sourceforge.net/events/workshop-0508.html> and contact Peter Mehlitz at <Pet...@na...> if you are interested to attend or give a talk. Hope to see you there -- the JPF team |
|
From: <pcm...@us...> - 2008-02-01 18:45:16
|
Revision: 741
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=741&view=rev
Author: pcmehlitz
Date: 2008-02-01 10:45:06 -0800 (Fri, 01 Feb 2008)
Log Message:
-----------
* added an Verify.setProperties(String...p) to programmatically set JPF properties at runtime from within the
model
* using this, extended the TestContracts example to show how to implement NativePredicates that are backtracking aware
- nice demo!
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-02-01 07:21:24
|
Revision: 740
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=740&view=rev
Author: pcmehlitz
Date: 2008-01-31 23:21:22 -0800 (Thu, 31 Jan 2008)
Log Message:
-----------
* some more java.util.Random methods (but CGs for the enumerate_random mode still missing)
* seamless integration of native and model properties. Maybe it's a bit too seamless, since
both implement the same interface (Predicate), but in all likeliness differ substantially in
implementation (the 'Object' parameters are different). Worked around that by adding a type tag
interface 'NativePredicate' but that's not very type safe.
The Satisfies predicate lookup had to be changed in order to avoid confusion when executing JPF
with the native predicates in the JPF classpath (e.g. when running from within Eclipse)
* added a native example predicate 'IsMonotonicDecreasing', which shows why we might want native
predicates (carries state we don't want in the model). Isn't checked for proper backtracking behavior yet
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/src/gov/nasa/jpf/test/ContractContext.java
trunk/src/gov/nasa/jpf/test/Satisfies.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/ExecBounds.java
trunk/app/gov/nasa/jpf/NoAlloc.java
trunk/app/gov/nasa/jpf/NoBlock.java
trunk/src/gov/nasa/jpf/test/NativePredicate.java
trunk/src/gov/nasa/jpf/test/predicate/
trunk/src/gov/nasa/jpf/test/predicate/IsMonotonicDecreasing.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/test/Predicate.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-30 02:10:16
|
Revision: 739
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=739&view=rev
Author: pcmehlitz
Date: 2008-01-29 18:10:12 -0800 (Tue, 29 Jan 2008)
Log Message:
-----------
* bug in propagation of double-word local slots (the "?" fillers screwed up the slot offset calculation when
retrieving the lvar)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-29 05:19:47
|
Revision: 738
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=738&view=rev
Author: pcmehlitz
Date: 2008-01-28 21:19:44 -0800 (Mon, 28 Jan 2008)
Log Message:
-----------
start to roll in missing contract extensions, but not yet complete
* model space contracts - still needs some polishing, and needs to be aligned with native properties (with which it
shares the same interface in app/). This also requires @Local to be implemeted, to provide additional safeguards
against contract side effects. It's debatable if the model should be "just call arbitrary user code" or "only
allow very restricted user code" to avoid side effects on the state space. For now, we go with the second one, otherwise
we have to introduce a synthetic wrapper around contracted method calls. The reason is that I see this as a last
measure anyways, and expect the majority of contract types to be built-in or native side
@Local could be a very useful property on its own, think I do this next as a complement to @Const (which also needs
to be integrated into ContractVerifier)
* had to refactor Contract for this, pulling the generic Satisfies to toplevel
* added very minimalistic support for DateFormat parsing
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractContext.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/Local.java
trunk/app/gov/nasa/jpf/Predicate.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DateFormat.java
trunk/src/gov/nasa/jpf/test/Satisfies.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-28 22:10:59
|
Revision: 737
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=737&view=rev
Author: pcmehlitz
Date: 2008-01-28 14:10:56 -0800 (Mon, 28 Jan 2008)
Log Message:
-----------
* the stupid metrics builder sneaked into the Eclipse project properties again. Don't know how often I still have to remove it until it sticks
Modified Paths:
--------------
trunk/.project
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-26 02:21:59
|
Revision: 736
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=736&view=rev
Author: pcmehlitz
Date: 2008-01-25 18:21:57 -0800 (Fri, 25 Jan 2008)
Log Message:
-----------
* we were cutting corners on the interned strings, and actually weren't using them internally (e.g. for class names).
It would have been possible to hit a new state branch that re-used the same ElementInfo for another string, in
which - unlikely - case we would have returned a wrong string object. Write 100 times: "never cut corners"
the alternatives would be a backtrackable HashMap<String,Integer>, or a container struct on the model side. But
efficient lookup would require model code (we can't easily call from the native side), or a dumb array, which
would have been bad for state storage upon change
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LDC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LDC_W.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-25 18:47:31
|
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.
|
|
From: <pcm...@us...> - 2008-01-22 22:58:48
|
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.
|
|
From: <pcm...@us...> - 2008-01-18 22:50:50
|
Revision: 733
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=733&view=rev
Author: pcmehlitz
Date: 2008-01-18 14:50:49 -0800 (Fri, 18 Jan 2008)
Log Message:
-----------
* wrong signature in sun.misc.Unsafe peer (but the putObject is still not implemented)
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sj...@us...> - 2008-01-18 21:23:37
|
Revision: 732
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=732&view=rev
Author: sjp100
Date: 2008-01-18 13:23:36 -0800 (Fri, 18 Jan 2008)
Log Message:
-----------
removed debug statements
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sj...@us...> - 2008-01-18 21:21:40
|
Revision: 731
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=731&view=rev
Author: sjp100
Date: 2008-01-18 13:21:32 -0800 (Fri, 18 Jan 2008)
Log Message:
-----------
fixed listener to work with new naming scheme for symbolic
and concrete values (properly gets them from the stack frame)
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-16 19:59:39
|
Revision: 730
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=730&view=rev
Author: pcmehlitz
Date: 2008-01-16 11:59:37 -0800 (Wed, 16 Jan 2008)
Log Message:
-----------
* forgot to quote '[' and ']' in StringSetMatcher patterns, which made NativeStateMachine receiver
matching fail in case of state array fields
Modified Paths:
--------------
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.
|
|
From: <pc...@us...> - 2008-01-16 02:33:13
|
Revision: 729
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=729&view=rev
Author: pcorina
Date: 2008-01-15 18:33:12 -0800 (Tue, 15 Jan 2008)
Log Message:
-----------
added patches created by Adam Kiezun (ak...@gm...)
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryLinearIntegerExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryNonLinearIntegerExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryRealExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Comparator.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Expression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/GreaterEqual.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/GreaterThan.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/IntegerConstant.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/IntegerExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/LinearIntegerExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Operator.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/PathCondition.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/RealExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicConstraintsChoco.java
Removed Paths:
-------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/DivideBy.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Equal.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/LessEqual.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/LessThan.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Minus.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/MultiplyBy.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/NotEqual.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Plus.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-01-16 02:30:09
|
Revision: 728
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=728&view=rev
Author: pcorina
Date: 2008-01-15 18:29:55 -0800 (Tue, 15 Jan 2008)
Log Message:
-----------
added patches created by Adam Kiezun (ak...@gm...)
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/D2I.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/D2L.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DCMPG.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/DREM.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DSUB.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/F2I.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/F2L.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FCMPG.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FCMPL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FDIV.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FMUL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FNEG.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FREM.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FSUB.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/I2D.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/I2F.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_ICMPEQ.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/IF_ICMPNE.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/L2D.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/L2F.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/LCMP.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/LMUL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/LSHL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/LSHR.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/LUSHR.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2008-01-16 01:37:34
|
Revision: 727
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=727&view=rev
Author: pcorina
Date: 2008-01-15 17:36:14 -0800 (Tue, 15 Jan 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DDIV.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-09 01:31:09
|
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.
|
|
From: <ubn...@us...> - 2008-01-08 19:55:58
|
Revision: 725
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=725&view=rev
Author: ubnepvpb
Date: 2008-01-08 11:55:53 -0800 (Tue, 08 Jan 2008)
Log Message:
-----------
Bug 1863583 from adam_kiezun, gov.nasa.jpf.symbc.bytecode.FCMPG should extend gov.nasa.jpf.jvm.bytecode.FCMPG, not gov.nasa.jpf.jvm.bytecode.FCMPL
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FCMPG.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
