| java.lang.Object
 gov.nasa.jpf.JPF
| JPF | | public class JPF implements Runnable(Code) | | main class of the JPF verification framework. This reads the configuration,
instantiates the Search and VM objects, and kicks off the Search
|
| Constructor Summary | |
| public | JPF(Config conf)
create new JPF object. |
| VERSION | | static String VERSION(Code) | | JPF version, we read this inlater from default.properties
|
| jpf | | static JPF jpf(Code) | | the singleton driver object, so that we can override FactoryMethods
|
| path | | Path path(Code) | | this is a pre-recorded path, NOT one freshly produced by a property
violation
|
| search | | public Search search(Code) | | The search engine used to visit the state space.
|
| vm | | public VM vm(Code) | | Reference to the virtual machine used by the model checker.
|
| JPF | | public JPF(Config conf)(Code) | | create new JPF object. Note this is always guaranteed to return, but the
Search and/or VM object instantiation might have failed (i.e. the JPF
object might not be really usable). If you directly use getSearch() / getVM(),
check for null
|
| checkUnknownArgs | | static void checkUnknownArgs(String[] args)(Code) | | this assumes that we have checked and 'consumed' (nullified) all known
options, so we just have to check for any '-' option prior to the
target class name
|
| createConfig | | public static Config createConfig(String[] args)(Code) | | return a Config object that holds the JPF options. This first
loads the properties from a (potentially configured) properties file, and
then overlays all command line arguments that are key/value pairs
|
| exit | | public static void exit()(Code) | | |
| foundErrors | | public boolean foundErrors()(Code) | | |
| getArg | | static String getArg(String[] args, String pattern, String defValue, boolean consume)(Code) | | find the value of an arg that is either specific as
"-key=value" or as "-key value". If not found, the supplied
defValue is returned
|
| getConfigFileName | | static String getConfigFileName(String[] args)(Code) | | what property file to look for
|
| getLogger | | public static Logger getLogger(String name)(Code) | | use this one to get a Logger that is initialized via our Config mechanism. Note that
our own Loggers do NOT pass
|
| getRootDirName | | static String getRootDirName(String[] args)(Code) | | where to look for the file (if it's not in the current dir)
|
| getSearch | | public Search getSearch()(Code) | | return the search object. This can be null if the initialization has failed
|
| getVM | | public VM getVM()(Code) | | return the VM object. This can be null if the initialization has failed
|
| isHelpRequest | | static boolean isHelpRequest(String[] args)(Code) | | |
| isPrintConfigRequest | | static boolean isPrintConfigRequest(String[] args)(Code) | | |
| isRunnable | | public boolean isRunnable()(Code) | | |
| printBanner | | public static void printBanner(Config config)(Code) | | |
| run | | public void run()(Code) | | runs the verification.
|
| showUsage | | static void showUsage()(Code) | | |
|
|