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

[<pcm...@us...>]

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.