added class name to warning for ambiguous native methods (without MJI signatures)

the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up

streamlined class init, which was a mixed case of registerClass()/initializeClass() and pushRequiredClinits(). Now it is a single initializeClass(ti) method which combines the previous initializeClass(), pushRequiredClinits() and pushClinit() methods. The reason for combining these is the forthcoming replacement of separately locked clinits from different DirectCallStackFrames with a single synthetic frame that calls clinits from nested synchronized blocks. This is required to model hotspot, which does cause deadlocks with concurrent init of classes that cause subclass init during their clinit executions.

fixed JPF_.._Verify.registerChoiceGenerator() to not break and ignore the

reshuffled Event hierarchy, introducing SystemEvent, with CheckEvent and

changed EventForest to derive from EventTree, which kills three birds with one

!!! NOTE: this marks the beginning of Java 8 dependency for jpf-core compilation.

moved LogConsole to .jpf.tool package

added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked

fixed forgotten ClInitRequired check in DateFormat - thanks to Jiri Vahala

some minor syntax fixes to make IntelliJ happy

bug caused by using the wrong index during scheduler.updateArraySharedness() -

replaced ThreadInfo.yield() (which was bypassing SyncPolicy) with SyncPolicy.setsRescheduleCG(). The current use is only for the corner case where the last transition in the last non-daemon triggers a defect in a still runnable daemon, which we want to detect before the daemon is shut down.

modified PathOutputMonitor to allow in-situ path specs. If the pom.{all|any|none} value starts with a double quote it is taken as the output spec. Also added a VerbatimOutputSpec in case we don't want regex matching

PairPermutationGenerator didn't have public ctor