Package | Description |
---|---|
gov.nasa.jpf.util.test | |
gov.nasa.jpf.vm |
Modifier and Type | Class and Description |
---|---|
class |
JPF_gov_nasa_jpf_util_test_TestJPF
native peer for our test class root
|
class |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF |
Modifier and Type | Class and Description |
---|---|
class |
AtomicFieldUpdater
base class for atomic field updaters
NOTE - since all native methods are static, we have to be too
|
class |
JPF_gov_nasa_jpf_AnnotationProxyBase
native peer for Annotation Proxies
(saves us some bytecode interpretation shoe leather)
|
class |
JPF_gov_nasa_jpf_CachedROHttpConnection
very simple URLConnection model that can be used for reading static URL contents
The data can be stored in/read from the file system, and is cached
to avoid DOS by means of model checking
|
class |
JPF_gov_nasa_jpf_ConsoleOutputStream
MJI NativePeer class to intercept all System.out and System.err
printing.
|
class |
JPF_gov_nasa_jpf_DelegatingTimeZone
native peer for JPFs concrete TimeZone class, which is just delegating to the
host VM so that we are independent of Java versions
|
class |
JPF_gov_nasa_jpf_SerializationConstructor |
class |
JPF_gov_nasa_jpf_test_MemoryGoal
native peer for MemoryGoal tests
|
class |
JPF_gov_nasa_jpf_tools_MethodTester
native peer for the MethodTester tool
|
class |
JPF_gov_nasa_jpf_vm_Verify
native peer class for programmatic JPF interface (that can be used inside
of apps to verify - if you are aware of the danger that comes with it)
this peer is a bit different in that it only uses static fields and methods because
its use is supposed to be JPF global (without classloader namespaces)
|
class |
JPF_java_io_File
intercept and forward some of the filesystem access methods.
|
class |
JPF_java_io_FileDescriptor
native peer for file descriptors, which are our basic interface to
access file contents.
|
class |
JPF_java_io_InputStreamReader |
class |
JPF_java_io_ObjectInputStream |
class |
JPF_java_io_ObjectOutputStream |
class |
JPF_java_io_ObjectStreamClass |
class |
JPF_java_io_OutputStreamWriter
native peer for OutputStreamWriter, to avoid that we have the
char-to-byte conversion in JPF
<2do> this needs to be de-staticed (see model class)
|
class |
JPF_java_io_RandomAccessFile
MJI NativePeer class for java.io.RandomAccessFile library abstraction
|
class |
JPF_java_lang_Boolean |
class |
JPF_java_lang_Byte |
class |
JPF_java_lang_Character
MJI NativePeer class for java.lang.Character library abstraction
Whoever is using this seriously is definitely screwed, performance-wise
|
class |
JPF_java_lang_Class
MJI NativePeer class for java.lang.Class library abstraction
|
class |
JPF_java_lang_ClassLoader |
class |
JPF_java_lang_Double
MJI NativePeer class for java.lang.Double library abstraction
|
class |
JPF_java_lang_Float
MJI NativePeer class for java.lang.Float library abstraction
|
class |
JPF_java_lang_Integer
MJI NativePeer class for java.lang.Integer library abstraction
|
class |
JPF_java_lang_Long
MJI NativePeer class for java.lang.Long library abstraction
|
class |
JPF_java_lang_Math
MJI NativePeer class for java.lang.Math library abstraction
|
class |
JPF_java_lang_Object
MJI NativePeer class for java.lang.Object library abstraction
|
class |
JPF_java_lang_reflect_Array
MJI NativePeer class for java.lang.reflect.Array library abstraction
|
class |
JPF_java_lang_reflect_Constructor
native peer for rudimentary constructor reflection.
|
class |
JPF_java_lang_reflect_Field |
class |
JPF_java_lang_reflect_Method |
class |
JPF_java_lang_reflect_Proxy |
class |
JPF_java_lang_Runtime
just a dummy for now, to avoid UnsatisfiedLinkErrors
|
class |
JPF_java_lang_Short
MJI NativePeer class for java.lang.Short library abstraction
|
class |
JPF_java_lang_String
MJI NativePeer class for java.lang.String library abstraction
|
class |
JPF_java_lang_StringBuffer
MJI NativePeer class for java.lang.StringBuffer library abstraction
|
class |
JPF_java_lang_StringBuilder |
class |
JPF_java_lang_StringCoding
we are not really interested in model checking this, so we intercept
and ignore
<2do> at some point we should probably do proper decoding/encoding,
but the java.lang.StringCoding class is unfortunately not public,
and it would be a pain to work around the access restrictions
|
class |
JPF_java_lang_System
MJI NativePeer class for java.lang.System library abstraction
|
class |
JPF_java_lang_Thread
MJI NativePeer class for java.lang.Thread library abstraction
NOTE - this implementation depends on all live thread objects being
in ThreadList
|
class |
JPF_java_lang_Throwable
MJI NativePeer class for java.lang.Throwable library abstraction
|
class |
JPF_java_net_URLClassLoader |
class |
JPF_java_net_URLDecoder
native peer for java.net.URLDecoder forwarding
|
class |
JPF_java_net_URLEncoder
native peer for java.net.URLEncoder forwarding
|
class |
JPF_java_security_MessageDigest |
class |
JPF_java_text_Bidi |
class |
JPF_java_text_DateFormat
this is just the minimal support for DateFormat.parse(String)
|
class |
JPF_java_text_DateFormatSymbols |
class |
JPF_java_text_DecimalFormat |
class |
JPF_java_text_DecimalFormatSymbols
MJI NativePeer class for java.text.DecimalFormatSymbols library abstraction
we need to intercept the initialization because it is requires
file io (properties) based on the Locale
|
class |
JPF_java_text_Format
native peer for java.text.Format delegation.
|
class |
JPF_java_text_SimpleDateFormat
(incomplete) native peer for SimpleDateFormat.
|
class |
JPF_java_util_Calendar |
class |
JPF_java_util_concurrent_atomic_AtomicInteger
native peer for java.util.concurrent.atomic.AtomicInteger
this implementation just cuts off native methods
|
class |
JPF_java_util_concurrent_atomic_AtomicIntegerArray
native peer for java.util.concurrent.atomic.AtomicIntegerArray
|
class |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater
a full peer for the AtomicIntegerFieldUpdater
|
class |
JPF_java_util_concurrent_atomic_AtomicLong
native peer for java.util.concurrent.atomic.AtomicLong
this implementation just cuts off native methods
|
class |
JPF_java_util_concurrent_atomic_AtomicLongArray
native peer for java.util.concurrent.atomic.AtomicLongArray
|
class |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater
a full peer for the AtomicLongFieldUpdater
|
class |
JPF_java_util_concurrent_atomic_AtomicReferenceArray
native peer for java.util.concurrent.atomic.AtomicReferenceArray
|
class |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater
a full peer for the AtomicReferenceFieldUpdater
|
class |
JPF_java_util_Date |
class |
JPF_java_util_Locale |
class |
JPF_java_util_logging_Level
this is only a skeleton to make basic logging work under JPF
|
class |
JPF_java_util_Random
MJI NativePeer class for java.util.Random library abstraction
model - peer delegation is done via restoring a singleton, which unfortunately
has to resort to the rather nasty Unsafe mechanism because the required
random internals are private.
|
class |
JPF_java_util_regex_Matcher
native peer for a regex Matcher
this is just a delegatee peer
|
class |
JPF_java_util_regex_Pattern |
class |
JPF_java_util_ResourceBundle
native peer for ResourceBundle
|
class |
JPF_java_util_TimeZone
native peer for java.util.TimeZone
this is a (mostly) delegating implementation that became necessary because TimeZone has been
considerably changed in Java 1.7 (OpenJDK) and we need a version that is compatible with
pre and post 1.7 releases
|
class |
JPF_sun_misc_Hashing
simple forwarding sun.misc.Hashing peer to speed up execution and shorten traces
|
class |
JPF_sun_misc_Unsafe
we don't want this class! This is a hodgepodge of stuff that shouldn't be in Java, but
is handy for some hacks.
|
class |
JPF_sun_misc_VM
this is just a placeholder for now, we don't support its functionality
|
class |
JPF_sun_net_www_protocol_http_Handler
native peer to configure concrete URLConnection classes for specific URLs
We use model class configuration in case somebody wants to implement logic
in there that requires backtracking, and doesn't want to do this on the
native peer level
example config:
http.connection= http://*.dtd => gov.nasa.jpf.CachedROHttpConnection, http://foo.com/* -- x.y.MyHttpConnection
|
class |
JPF_sun_reflect_Reflection |
class |
JPF_sun_reflect_ReflectionFactory
<2do> hack around a hack - we need to override this as long as we don't
replace ObjectStreamClass
|
Modifier and Type | Field and Description |
---|---|
protected NativePeer |
NativeMethodInfo.peer |
Modifier and Type | Method and Description |
---|---|
NativePeer |
ClassInfo.getNativePeer() |
NativePeer |
NativeMethodInfo.getNativePeer() |
protected NativePeer |
ClassInfo.loadNativePeer() |
Constructor and Description |
---|
NativeMethodInfo(MethodInfo mi,
Method mth,
NativePeer peer) |