Modifier and Type | Method and Description |
---|---|
static Config |
JPF.createConfig(String[] args)
return a Config object that holds the JPF options.
|
Config |
JPF.getConfig() |
Config |
Config.reload() |
Modifier and Type | Method and Description |
---|---|
void |
ConfigChangeListener.jpfRunTerminated(Config conf)
this can be used to let a config listener remove itself, which is
required if the same Config object is used for several JPF runs
|
static void |
JPF.printBanner(Config config) |
void |
ConfigChangeListener.propertyChanged(Config conf,
String key,
String oldValue,
String newValue)
a JPF property was changed during runtime (e.g.
|
static void |
JPF.start(Config conf,
String[] args) |
Constructor and Description |
---|
JPF(Config conf)
create new JPF object.
|
Constructor and Description |
---|
DefaultJVMClassFactory(Config config) |
Modifier and Type | Method and Description |
---|---|
static void |
FieldInstruction.init(Config config) |
Modifier and Type | Method and Description |
---|---|
protected void |
Perturbator.addToFieldWatchList(Config conf,
String id) |
protected void |
Perturbator.addToParamsWatchList(Config conf,
String id) |
protected void |
Perturbator.addToReturnWatchList(Config conf,
String id) |
protected List<gov.nasa.jpf.listener.CGRemover.Category> |
CGRemover.parseCategories(Config conf) |
void |
SearchMonitor.run(Config conf) |
Constructor and Description |
---|
GenericDataAbstractor(Config conf,
String keyPrefix) |
IntOverUnder(Config conf,
String keyPrefix) |
Modifier and Type | Field and Description |
---|---|
protected Config |
Reporter.conf |
protected Config |
Publisher.conf |
Constructor and Description |
---|
ConsolePublisher(Config conf,
Reporter reporter) |
Publisher(Config conf,
Reporter reporter) |
Reporter(Config conf,
JPF jpf) |
XMLPublisher(Config conf,
Reporter reporter) |
Modifier and Type | Field and Description |
---|---|
protected Config |
Search.config |
Modifier and Type | Method and Description |
---|---|
Config |
Search.getConfig() |
Modifier and Type | Method and Description |
---|---|
protected ArrayList<Property> |
Search.getProperties(Config config)
return set of configured properties
note there is a name clash here - JPF 'properties' have nothing to do with
Java properties (java.util.Properties)
|
protected void |
Search.initialize(Config conf) |
Constructor and Description |
---|
DFSearch(Config config,
VM vm) |
PathSearch(Config config,
VM vm) |
RandomSearch(Config config,
VM vm) |
Search(Config config,
VM vm) |
Simulation(Config config,
VM vm) |
Constructor and Description |
---|
BFSHeuristic(Config config,
VM vm) |
DFSHeuristic(Config conf,
VM vm) |
GlobalSwitchThread(Config config,
VM vm) |
HeuristicSearch(Config config,
VM vm) |
Interleaving(Config config,
VM vm) |
MinimizePreemption(Config config,
VM vm) |
MostBlocked(Config config,
VM vm) |
PreferThreads(Config config,
VM vm) |
RandomHeuristic(Config config,
VM vm) |
SimplePriorityHeuristic(Config config,
VM vm) |
StaticPriorityQueue(Config config) |
UserHeuristic(Config config,
VM vm) |
Modifier and Type | Method and Description |
---|---|
static Config |
RunTest.getConfig() |
Modifier and Type | Method and Description |
---|---|
static void |
Source.init(Config config) |
static void |
LogManager.init(Config conf)
note - this is not allowed to fail, since we couldn't log that.
|
Constructor and Description |
---|
LogHandler(Config conf) |
Modifier and Type | Field and Description |
---|---|
protected Config |
EventGeneratorFactory.conf |
Modifier and Type | Method and Description |
---|---|
protected void |
TestJPF.setTestTargetKeys(Config conf,
StackTraceElement testMethod) |
protected void |
TestMultiProcessJPF.setTestTargetKeys(Config conf,
StackTraceElement testMethod) |
Modifier and Type | Field and Description |
---|---|
protected Config |
VM.config |
Modifier and Type | Method and Description |
---|---|
Config |
MJIEnv.getConfig() |
Config |
VM.getConfig() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
VM.getPlatformEndianness(Config config) |
static boolean |
JPF_java_lang_reflect_Field.init(Config conf) |
static boolean |
JPF_java_lang_reflect_Constructor.init(Config conf) |
static boolean |
JPF_java_lang_Class.init(Config conf) |
static boolean |
JPF_java_text_Format.init(Config conf) |
static boolean |
JPF_java_lang_reflect_Method.init(Config conf) |
static boolean |
SharedObjectPolicy.init(Config config) |
static boolean |
NativePeer.init(Config conf) |
static boolean |
JPF_gov_nasa_jpf_vm_Verify.init(Config conf) |
static void |
ChoiceGeneratorBase.init(Config config) |
static boolean |
HashedAllocationContext.init(Config conf) |
protected void |
GenericSGOIDHeap.initAllocationContext(Config config) |
void |
VM.initFields(Config config) |
protected void |
VM.initSubsystems(Config config) |
protected void |
VM.initTimeModel(Config config) |
static String |
ClassInfo.makeModelClassPath(Config config) |
Constructor and Description |
---|
DoubleChoiceFromList(Config conf,
String id) |
DoubleChoiceFromSet(Config conf,
String id) |
DoubleThresholdGenerator(Config conf,
String id) |
FloatChoiceFromList(Config conf,
String id) |
IntChoiceFromList(Config conf,
String id) |
IntChoiceFromSet(Config conf,
String id) |
IntIntervalGenerator(Config conf,
String id) |
LongChoiceFromList(Config conf,
String id) |
NumberChoiceFromList(Config conf,
String id) |
RandomIntIntervalGenerator(Config conf,
String id) |
TypedObjectChoice(Config conf,
String id) |
Modifier and Type | Field and Description |
---|---|
protected Config |
IgnoresFromAnnotations.config |
protected Config |
IncludesFromAnnotations.config |
Modifier and Type | Method and Description |
---|---|
protected void |
AmmendableFilterConfiguration.appendConfiguredFrameAmmendments(Config config) |
protected void |
AmmendableFilterConfiguration.appendConfiguredInstanceAmmendments(Config config) |
protected void |
AmmendableFilterConfiguration.appendConfiguredInstanceOverrides(Config config) |
protected void |
AmmendableFilterConfiguration.appendConfiguredStaticAmmendments(Config config) |
protected List<gov.nasa.jpf.vm.serialize.DynamicAbstractionSerializer.FieldAbstraction> |
DynamicAbstractionSerializer.getFieldAbstractions(Config conf) |
void |
AmmendableFilterConfiguration.init(Config config) |
void |
FilterConfiguration.init(Config config) |
void |
DefaultFilterConfiguration.init(Config config) |
Constructor and Description |
---|
DynamicAbstractionSerializer(Config conf) |
IgnoresFromAnnotations(Config config) |
IncludesFromAnnotations(Config config) |