Members/kono/jpf-core: jpf.properties comparison

comparison jpf.properties @ 0:61d41facf527

initial v8 import (history reset)

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Fri, 23 Jan 2015 10:14:01 -0800
parents
children	6774e2e08d37

comparison

equal deleted inserted replaced

--1:000000000000
+:61d41facf527
+# 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

Mercurial > hg > Members > kono > jpf-core

comparison jpf.properties @ 0:61d41facf527