# JPF configuration for "jpf-core" component # path elements can either be relative to the property file location, or # use the JPF component name (e.g. "jpf-core") as a variable prefix # (e.g. "jpf-core.sourcepath=${jpf-core}/src/examples"). # If a jpf.properties is to be used within NB, it has to use the variable prefix # (prepending the project root is only done during JPF init) # we use the ';' separator here because it is recognized by NetBeans (as opposed # to ',') # 'config_path' is set automatically by gov.nasa.jpf.Config during JPF init. # If used from within an Ant build system, 'jpf-core' has to be set explicitly # (ant does ${..} property expansion, but ignores property redefinition, so the # following line will be ignored) jpf-core = ${config_path} jpf-core.native_classpath=\ ${jpf-core}/build/jpf.jar;\ ${jpf-core}/build/jpf-annotations.jar jpf-core.classpath=\ ${jpf-core}/build/jpf-classes.jar;\ ${jpf-core}/build/examples jpf-core.sourcepath=\ ${jpf-core}/src/examples jpf-core.test_classpath=\ ${jpf-core}/build/tests jpf-core.peer_packages = gov.nasa.jpf.vm,, # the default jpf-core properties file with keys for which we need mandatory defaults ########################### 0. global part ############################### # instances that are both search and VM listeners #listener = .. # do we want JPF exceptions to print their stack traces (that's only for # debugging) jpf.print_exception_stack = true # this is where we can specify additional classpath entries that are # not in the system property class.path (e.g. when running JPF from # an environment that uses it's own loaders, like Eclipse plugins etc.) #jpf.native_classpath = .. ########################### 1. Search part ############################### search.class = gov.nasa.jpf.search.DFSearch # This flag indicates whether state matching will only be done when a state # is revisited at a lower depth. By default this is false. If it is set to # true and no error is found in a limited-depth search then it is guaranteed # not to have such error below that depth. Note that for traditional # depth limited search this does not hold search.match_depth = false # This flag indicates whether JPF should produce more than one error # or stop at the first one search.multiple_errors = false # the minimum free memory bounds. If we fall below that threshold, we # stop the search search.min_free = 1M # name of the file in which we store error paths. If not set, we don't store #search.error_path = error.xml # the standard properties we want to check for search.properties=\ gov.nasa.jpf.vm.NotDeadlockedProperty,\ gov.nasa.jpf.vm.NoUncaughtExceptionsProperty # various heuristic parameters # This number specifies the maximum number of states to keep on the queue # during a heuristic search. By default it is set to -1 search.heuristic.queue_limit = -1 # This flag indicates whether branches with counts less than branch-start # are to be ranked according to how many times they have been taken. # It is set to true by default. If it is set to false, they are all valued # the same search.heuristic.branch.count_early = true # This number determines at what point branches are heuristically valued as worse # than non-branching transitions. By default this value is 1. branch_start = 1 # This number if greater than 0 is returned as the heuristic value for # non-branching transitions. By default it is set to -1 in which case the # value of branch-start is returned instead search.heuristic.branch.no_branch_return = -1 # exclusive search listeners # search.listener = ############################### 2. VM part ############################### # this is an ordered list of packages from which we try to locate native peers. # "" means JPF tries the same package like the model class # "" means no package at all # (this is going to be extended by jpf.properties files) #peer_packages = , vm.class = gov.nasa.jpf.vm.SingleProcessVM # the ClassLoaderInfo class used for startup vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo # class used to hash/store states (if not set, states are not matched) vm.storage.class = gov.nasa.jpf.vm.JenkinsStateSet # class used to maintain the backtrack stack vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker # serializer to be used by state set (vm.storage.class) vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer #vm.serializer.class = gov.nasa.jpf.vm.serialize.AdaptiveSerializer #vm.serializer.class = gov.nasa.jpf.vm.serialize.FilteringSerializer # the class that models static fields and classes vm.statics.class = gov.nasa.jpf.vm.OVStatics # the class that models the heap #vm.heap.class = gov.nasa.jpf.vm.PSIMHeap vm.heap.class = gov.nasa.jpf.vm.OVHeap # the class representing the list of all threads vm.threadlist.class = gov.nasa.jpf.vm.ThreadList # restorer to be used by backtracker such as DefaultBacktracker UNLESS a # serializer that is also a restorer (such as CollapsingSerializer) is used. # I.e. this is only read if serializer is not used or it's not a StateRestorer vm.restorer.class = .vm.DefaultMementoRestorer # where do we get the standard libraries from? # "" is replaced by the host VM sun.boot.class.path setting vm.boot_classpath = # instruction factory jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory # fields factory vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory # pattern list for assertion enabled/disabled classes #vm.enable_assertions = * #vm.disable_assertions= # do we support the Verify.ignorePath() API (to imperatively ignore paths in modeled/instrumented programs)? vm.verify.ignore_path = true vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy # the following properties can be used to set filters for GenericSharednessPolicy instances # never break on exposure or shared field access from matching methods. # NOTE - this is transitive and hence should only include a minimal set of trusted methods vm.shared.never_break_methods=\ java.util.concurrent.ThreadPoolExecutor.processWorkerExit,\ java.util.concurrent.locks.Abstract*Synchronizer.*,\ java.util.concurrent.ThreadPoolExecutor.getTask,\ java.util.concurrent.atomic.Atomic*.*,\ java.util.concurrent.Exchanger.doExchange,\ java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,\ java.util.concurrent.TimeUnit.* vm.shared.never_break_types=\ java.util.concurrent.TimeUnit # never break on shared access of the following fields. While this is less prone to # masking defects than never_break_methods, it should also be used sparingly. # NOTE - java.lang.Thread* fields should not be excluded if the SUT explicitly uses # Thread or ThreadGroup objects vm.shared.never_break_fields=\ java.lang.Thread*.*,\ java.lang.System.*,\ java.lang.Runtime.*,\ java.lang.Boolean.*,\ java.lang.String.*,\ java.lang.*.TYPE,\ java.util.HashMap.EMPTY_TABLE,\ java.util.HashSet.PRESENT,\ java.util.concurrent.ThreadPoolExecutor*.*,\ java.util.concurrent.ThreadPoolExecutor*.*,\ java.util.concurrent.TimeUnit.*,\ java.util.concurrent.Exchanger.CANCEL,\ java.util.concurrent.Exchanger.NULL_ITEM,\ java.util.concurrent.Executors$DefaultThreadFactory.*,\ sun.misc.VM.*,\ sun.misc.SharedSecrets.*,\ sun.misc.Unsafe.theUnsafe,\ gov.nasa.jpf.util.test.TestJPF.* # do we also break transitions on reference field puts that could make the # referenced objects shared vm.shared.break_on_exposure = true # do we try to deduce if a field is supposed to be protected by a lock? In this # case, we stop to treat this field as a boundary step, but only if we see the lock vm.shared.sync_detection = true # do we assume final fields to be race-safe (not really true, esp. for # instance fields with references leaking from a ctor, but a good starting point) vm.shared.skip_finals=true # ClassLoaders synchronize the loading of a class. # Thus, static final fields can never be included in a race condition since only 1 thread is allowed to access the class while it is loading. # Defaulted to false to maintain backward compatibility in JPF vm.shared.skip_static_finals=false # When an object's constructor has returned, then the final fields can not be changed. # Thus, instance final fields can never be included in a race condition (unless the this reference is leaked from a constructor) # Defaulted to false to maintain backward compatibility in JPF vm.shared.skip_constructed_finals=false # do we ignore explicitly set Thread.UncaughtHandlers vm.ignore_uncaught_handler=false # do we treat returned Thread.UncaughtHandler.uncaughtException() calls as normal thread termination vm.pass_uncaught_handler=true # do we reclaim unused memory (run garbage collection) vm.gc = true # threshold after which number of allocations to perform a garbage collection # (even within the same transition, to avoid lots of short living objects) # -1 means never vm.max_alloc_gc = -1 # do we run finalizers on collected objects (only makes sense with garbage collection) vm.finalize = false # this is a preemption boundary specifying the max number of instructions after which we # break the current transition if there are other runnable threads vm.max_transition_length = 50000 # are thread ids of terminated threads with recycled thread objects reused when creating new # threads. This is required for programs that sequentially create many short living threads vm.reuse_tid = false # do we want to halt execution on each throw of an exception that matches # one of the given classname wildcard patterns w/o looking for exception handlers? # (useful for empty handler blocks, over-permissive catches or generally # misused exceptions) #vm.halt_on_throw = * # class that is used to create scheduling relevant choice generators. # this will replace the scheduler vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory # print output as it is generated during the search (for all paths) vm.tree_output = true # collect output inside the stored path (to create program trace outout) vm.path_output = false # do we want to store the whole path no matter if we report them vm.store_steps=false # untracked property vm.untracked = true # from where do we initialize the system properties # SELECTED - keys specified as vm.system.properties, values from host # FILE - Java properties file (key=value pairs) # HOST - all system properties from underlying host VM vm.sysprop.source = SELECTED # pathname of property file with system properties #vm.sysprop.file = # list of key names to load from host VM #vm.sysprop.keys = # class we use to model execution time vm.time.class = gov.nasa.jpf.vm.SystemTime # if this is set to true, we throw an exception if we encounter any orphan native peer methods vm.no_orphan_methods = false # if this is set to true, overriden finalize() methods execute upon objects garbage collections vm.process_finalizers = false ### jvm specifics # di=o we model nested locks during class init (to detect possible hotspot dealocks during init) # (off by default since it can cause state explosion) jvm.nested_init=false # if so, for which classes (default is to exclude system classes) jvm.nested_init.exclude=java.*,javax.*,sun.misc.* ############################### 3. CG part ############################### # choice randomization policy in effect: # "NONE" - choice sets are not randomized # "FIXED_SEED" - choice sets are randomized using a fixed seed for each JPF run (reproducible) # "VAR_SEED" - choice sets are randomized using a variable seed for each JPF run cg.randomize_choices = NONE # the standard seed value used for the FIXED_SEED policy cg.seed = 42 # if this is set, we create choice generators even if there is only a single # choice. This is to ensure state storage/matching at all locations where a # choice generator *could* be created. The default should be to turn it off though, # since this can produce a lot of additional states (esp. with threads) cg.break_single_choice = false # default BooleanChoiceGenerator sequence: do we start with 'false' cg.boolean.false_first = true # do we want java.util.Random. nextXX() enumerate choices, or just return a single value? # (isn't implemented for all types yet) cg.enumerate_random=false # maximum number of processors returned by Runtime.availableProcessors(). If this is # greater than 1, the call represents a ChoiceGenerator cg.max_processors=1 # creates a CG upon Thread.start, i.e. breaks the starting transition. Note this is # required for data race detection (which depends on detecting access of shared objects) cg.threads.break_start=true # if this option is set we break the transition on Thread.yield() cg.threads.break_yield=true # if this option is set we break the transition on Thread.sleep() cg.threads.break_sleep=true # set if we shold also break on array instructions, e.g. to detect races # for array elements. This is off by default because it can cause serious # state explosion cg.threads.break_arrays=false # do we support atomic sections. If set to false, Verify.beginAtomic()/endAtomic() # will not do anything cg.enable_atomic=true ############################### 3. Report Part ############################### log.handler.class=gov.nasa.jpf.util.LogHandler # Windows seem to have a different default log.level=warning report.class=gov.nasa.jpf.report.Reporter report.publisher=console report.console.class=gov.nasa.jpf.report.ConsolePublisher # this prints out repository information if the 'jpf' topic is set (for debugging) #jpf.report.show_repository=true #property violation reporting is configured separately report.console.start=jpf,sut report.console.transition= report.console.constraint=constraint,snapshot report.console.probe=statistics report.console.property_violation=error,snapshot report.console.show_steps=true report.console.show_method=true report.console.show_code=false report.console.finished=result,statistics #jpf.report.console.show_steps=true #jpf.report.console.show_method=true #jpf.report.console.show_code=true report.xml.class=gov.nasa.jpf.report.XMLPublisher report.html.class=gov.nasa.jpf.report.HTMLPublisher report.html.start=jpf,sut,platform,user,dtg,config report.html.constraint=constraint report.html.property_violation= report.html.finished=result,statistics,error,snapshot,output ############################### 4. Listener part ############################# # imperative list of listeners #listener= listener.autoload=\ gov.nasa.jpf.NonNull,\ gov.nasa.jpf.Const listener.gov.nasa.jpf.NonNull=gov.nasa.jpf.tools.NonNullChecker listener.gov.nasa.jpf.Const=gov.nasa.jpf.tools.ConstChecker ### PreciseRaceDetector # we don't check for races in standard libraries race.exclude=java.*,javax.* ############################### 5. test part ############################# test.report.console.finished=result