Mercurial > hg > Members > kono > jpf-core
view jpf.properties @ 19:9fea3d8da9aa
!!! NOTE: this marks the beginning of Java 8 dependency for jpf-core compilation.
From now on, we are free to use default methods and lambdas.
added convenience Loggable and PrintStreamable interfaces that mix in the
respective fat interfaces via default methods, so that we don't have to burn
inheritance of respective target classes (they only have to provide getLogger()
and getPrintStream() methods)
added a abstract LoggablePeer so that model classes can implement Loggable with
intercepted/native logging if they provide a respective concrete peer.
added some more default interface method tests
author | Peter Mehlitz <pcmehlitz@gmail.com> |
---|---|
date | Wed, 01 Apr 2015 12:14:15 -0700 |
parents | 61d41facf527 |
children | 6774e2e08d37 |
line wrap: on
line source
# 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,<model>,<default> # 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. # "<model>" means JPF tries the same package like the model class # "<default>" means no package at all # (this is going to be extended by jpf.properties files) #peer_packages = <model>,<default> 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? # "<system>" is replaced by the host VM sun.boot.class.path setting vm.boot_classpath = <system> # 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 ############################### 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