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

annotate jpf.properties @ 34:49be04cc6389 default tip java9-try

cyclic dependency ...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 19 Dec 2017 11:21:23 +0900
parents	6774e2e08d37
children

rev	line source
0 61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	1 # JPF configuration for "jpf-core" component
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	2
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	3 # path elements can either be relative to the property file location, or
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	4 # use the JPF component name (e.g. "jpf-core") as a variable prefix
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	5 # (e.g. "jpf-core.sourcepath=${jpf-core}/src/examples").
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	6 # If a jpf.properties is to be used within NB, it has to use the variable prefix
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	7 # (prepending the project root is only done during JPF init)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	8
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	9 # we use the ';' separator here because it is recognized by NetBeans (as opposed
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	10 # to ',')
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	11
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	12 # 'config_path' is set automatically by gov.nasa.jpf.Config during JPF init.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	13 # If used from within an Ant build system, 'jpf-core' has to be set explicitly
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	14 # (ant does ${..} property expansion, but ignores property redefinition, so the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	15 # following line will be ignored)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	16
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	17 jpf-core = ${config_path}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	18
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	19 jpf-core.native_classpath=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	20 ${jpf-core}/build/jpf.jar;\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	21 ${jpf-core}/build/jpf-annotations.jar
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	22
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	23 jpf-core.classpath=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	24 ${jpf-core}/build/jpf-classes.jar;\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	25 ${jpf-core}/build/examples
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	26
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	27 jpf-core.sourcepath=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	28 ${jpf-core}/src/examples
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	29
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	30 jpf-core.test_classpath=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	31 ${jpf-core}/build/tests
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	32
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	33 jpf-core.peer_packages = gov.nasa.jpf.vm,<model>,<default>
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	34
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	35
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	36
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	37 # the default jpf-core properties file with keys for which we need mandatory defaults
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	38
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	39 ########################### 0. global part ###############################
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	40
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	41 # instances that are both search and VM listeners
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	42 #listener = ..
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	43
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	44 # do we want JPF exceptions to print their stack traces (that's only for
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	45 # debugging)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	46 jpf.print_exception_stack = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	47
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	48
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	49 # this is where we can specify additional classpath entries that are
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	50 # not in the system property class.path (e.g. when running JPF from
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	51 # an environment that uses it's own loaders, like Eclipse plugins etc.)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	52 #jpf.native_classpath = ..
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	53
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	54
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	55 ########################### 1. Search part ###############################
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	56 search.class = gov.nasa.jpf.search.DFSearch
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	57
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	58
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	59 # This flag indicates whether state matching will only be done when a state
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	60 # is revisited at a lower depth. By default this is false. If it is set to
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	61 # true and no error is found in a limited-depth search then it is guaranteed
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	62 # not to have such error below that depth. Note that for traditional
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	63 # depth limited search this does not hold
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	64 search.match_depth = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	65
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	66 # This flag indicates whether JPF should produce more than one error
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	67 # or stop at the first one
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	68 search.multiple_errors = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	69
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	70 # the minimum free memory bounds. If we fall below that threshold, we
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	71 # stop the search
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	72 search.min_free = 1M
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	73
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	74 # name of the file in which we store error paths. If not set, we don't store
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	75 #search.error_path = error.xml
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	76
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	77 # the standard properties we want to check for
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	78 search.properties=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	79 gov.nasa.jpf.vm.NotDeadlockedProperty,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	80 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	81
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	82
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	83 # various heuristic parameters
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	84
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	85 # This number specifies the maximum number of states to keep on the queue
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	86 # during a heuristic search. By default it is set to -1
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	87 search.heuristic.queue_limit = -1
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	88
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	89 # This flag indicates whether branches with counts less than branch-start
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	90 # are to be ranked according to how many times they have been taken.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	91 # It is set to true by default. If it is set to false, they are all valued
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	92 # the same
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	93 search.heuristic.branch.count_early = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	94
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	95 # This number determines at what point branches are heuristically valued as worse
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	96 # than non-branching transitions. By default this value is 1.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	97 branch_start = 1
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	98
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	99
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	100 # This number if greater than 0 is returned as the heuristic value for
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	101 # non-branching transitions. By default it is set to -1 in which case the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	102 # value of branch-start is returned instead
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	103 search.heuristic.branch.no_branch_return = -1
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	104
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	105 # exclusive search listeners
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	106 # search.listener =
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	107
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	108
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	109 ############################### 2. VM part ###############################
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	110
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	111
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	112 # this is an ordered list of packages from which we try to locate native peers.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	113 # "<model>" means JPF tries the same package like the model class
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	114 # "<default>" means no package at all
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	115 # (this is going to be extended by jpf.properties files)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	116 #peer_packages = <model>,<default>
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	117
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	118
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	119 vm.class = gov.nasa.jpf.vm.SingleProcessVM
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	120
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	121 # the ClassLoaderInfo class used for startup
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	122 vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	123
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	124 # class used to hash/store states (if not set, states are not matched)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	125 vm.storage.class = gov.nasa.jpf.vm.JenkinsStateSet
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	126
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	127 # class used to maintain the backtrack stack
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	128 vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	129
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	130 # serializer to be used by state set (vm.storage.class)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	131 vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	132 #vm.serializer.class = gov.nasa.jpf.vm.serialize.AdaptiveSerializer
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	133 #vm.serializer.class = gov.nasa.jpf.vm.serialize.FilteringSerializer
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	134
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	135 # the class that models static fields and classes
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	136 vm.statics.class = gov.nasa.jpf.vm.OVStatics
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	137
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	138 # the class that models the heap
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	139 #vm.heap.class = gov.nasa.jpf.vm.PSIMHeap
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	140 vm.heap.class = gov.nasa.jpf.vm.OVHeap
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	141
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	142 # the class representing the list of all threads
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	143 vm.threadlist.class = gov.nasa.jpf.vm.ThreadList
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	144
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	145 # restorer to be used by backtracker such as DefaultBacktracker UNLESS a
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	146 # serializer that is also a restorer (such as CollapsingSerializer) is used.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	147 # I.e. this is only read if serializer is not used or it's not a StateRestorer
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	148 vm.restorer.class = .vm.DefaultMementoRestorer
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	149
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	150 # where do we get the standard libraries from?
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	151 # "<system>" is replaced by the host VM sun.boot.class.path setting
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	152 vm.boot_classpath = <system>
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	153
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	154 # instruction factory
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	155 jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	156
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	157 # fields factory
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	158 vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	159
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	160 # pattern list for assertion enabled/disabled classes
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	161 #vm.enable_assertions = *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	162 #vm.disable_assertions=
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	163
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	164 # do we support the Verify.ignorePath() API (to imperatively ignore paths in modeled/instrumented programs)?
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	165 vm.verify.ignore_path = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	166
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	167
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	168 vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	169 vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	170 vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	171
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	172 # the following properties can be used to set filters for GenericSharednessPolicy instances
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	173
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	174 # never break on exposure or shared field access from matching methods.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	175 # NOTE - this is transitive and hence should only include a minimal set of trusted methods
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	176 vm.shared.never_break_methods=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	177 java.util.concurrent.ThreadPoolExecutor.processWorkerExit,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	178 java.util.concurrent.locks.AbstractSynchronizer.,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	179 java.util.concurrent.ThreadPoolExecutor.getTask,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	180 java.util.concurrent.atomic.Atomic.,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	181 java.util.concurrent.Exchanger.doExchange,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	182 java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	183 java.util.concurrent.TimeUnit.*
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	184
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	185 vm.shared.never_break_types=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	186 java.util.concurrent.TimeUnit
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	187
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	188 # never break on shared access of the following fields. While this is less prone to
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	189 # masking defects than never_break_methods, it should also be used sparingly.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	190 # NOTE - java.lang.Thread* fields should not be excluded if the SUT explicitly uses
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	191 # Thread or ThreadGroup objects
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	192 vm.shared.never_break_fields=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	193 java.lang.Thread.,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	194 java.lang.System.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	195 java.lang.Runtime.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	196 java.lang.Boolean.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	197 java.lang.String.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	198 java.lang.*.TYPE,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	199 java.util.HashMap.EMPTY_TABLE,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	200 java.util.HashSet.PRESENT,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	201 java.util.concurrent.ThreadPoolExecutor.,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	202 java.util.concurrent.ThreadPoolExecutor.,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	203 java.util.concurrent.TimeUnit.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	204 java.util.concurrent.Exchanger.CANCEL,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	205 java.util.concurrent.Exchanger.NULL_ITEM,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	206 java.util.concurrent.Executors$DefaultThreadFactory.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	207 sun.misc.VM.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	208 sun.misc.SharedSecrets.*,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	209 sun.misc.Unsafe.theUnsafe,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	210 gov.nasa.jpf.util.test.TestJPF.*
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	211
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	212
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	213 # do we also break transitions on reference field puts that could make the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	214 # referenced objects shared
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	215 vm.shared.break_on_exposure = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	216
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	217 # do we try to deduce if a field is supposed to be protected by a lock? In this
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	218 # case, we stop to treat this field as a boundary step, but only if we see the lock
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	219 vm.shared.sync_detection = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	220
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	221 # do we assume final fields to be race-safe (not really true, esp. for
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	222 # instance fields with references leaking from a ctor, but a good starting point)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	223 vm.shared.skip_finals=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	224
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	225 # ClassLoaders synchronize the loading of a class.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	226 # 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.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	227 # Defaulted to false to maintain backward compatibility in JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	228 vm.shared.skip_static_finals=false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	229
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	230 # When an object's constructor has returned, then the final fields can not be changed.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	231 # Thus, instance final fields can never be included in a race condition (unless the this reference is leaked from a constructor)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	232 # Defaulted to false to maintain backward compatibility in JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	233 vm.shared.skip_constructed_finals=false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	234
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	235
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	236 # do we ignore explicitly set Thread.UncaughtHandlers
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	237 vm.ignore_uncaught_handler=false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	238
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	239 # do we treat returned Thread.UncaughtHandler.uncaughtException() calls as normal thread termination
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	240 vm.pass_uncaught_handler=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	241
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	242 # do we reclaim unused memory (run garbage collection)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	243 vm.gc = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	244
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	245 # threshold after which number of allocations to perform a garbage collection
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	246 # (even within the same transition, to avoid lots of short living objects)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	247 # -1 means never
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	248 vm.max_alloc_gc = -1
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	249
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	250 # do we run finalizers on collected objects (only makes sense with garbage collection)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	251 vm.finalize = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	252
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	253 # this is a preemption boundary specifying the max number of instructions after which we
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	254 # break the current transition if there are other runnable threads
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	255 vm.max_transition_length = 50000
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	256
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	257 # are thread ids of terminated threads with recycled thread objects reused when creating new
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	258 # threads. This is required for programs that sequentially create many short living threads
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	259 vm.reuse_tid = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	260
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	261 # do we want to halt execution on each throw of an exception that matches
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	262 # one of the given classname wildcard patterns w/o looking for exception handlers?
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	263 # (useful for empty handler blocks, over-permissive catches or generally
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	264 # misused exceptions)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	265 #vm.halt_on_throw = *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	266
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	267 # class that is used to create scheduling relevant choice generators.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	268 # this will replace the scheduler
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	269 vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	270
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	271 # print output as it is generated during the search (for all paths)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	272 vm.tree_output = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	273
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	274 # collect output inside the stored path (to create program trace outout)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	275 vm.path_output = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	276
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	277 # do we want to store the whole path no matter if we report them
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	278 vm.store_steps=false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	279
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	280 # untracked property
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	281 vm.untracked = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	282
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	283 # from where do we initialize the system properties
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	284 # SELECTED - keys specified as vm.system.properties, values from host
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	285 # FILE - Java properties file (key=value pairs)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	286 # HOST - all system properties from underlying host VM
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	287 vm.sysprop.source = SELECTED
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	288
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	289 # pathname of property file with system properties
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	290 #vm.sysprop.file =
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	291
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	292 # list of key names to load from host VM
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	293 #vm.sysprop.keys =
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	294
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	295 # class we use to model execution time
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	296 vm.time.class = gov.nasa.jpf.vm.SystemTime
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	297
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	298 # if this is set to true, we throw an exception if we encounter any orphan native peer methods
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	299 vm.no_orphan_methods = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	300
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	301 # if this is set to true, overriden finalize() methods execute upon objects garbage collections
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	302 vm.process_finalizers = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	303
24 6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	304
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	305 ### jvm specifics
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	306
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	307 # di=o we model nested locks during class init (to detect possible hotspot dealocks during init)
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	308 # (off by default since it can cause state explosion)
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	309 jvm.nested_init=false
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	310
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	311 # if so, for which classes (default is to exclude system classes)
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	312 jvm.nested_init.exclude=java.,javax.,sun.misc.*
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	313
6774e2e08d37 the fix I would have liked to avoid - apparently hotspot internally does nested locking during class init, which can lead to deadlocks such as described in http://ternarysearch.blogspot.ru/2013/07/static-initialization-deadlock.html. Actually, it's not a regular deadlock since core dumps still list the threads as runnable, althouth it doesn't seem to be a livelock either. In any case, it can be simulated by nested locking and clinit execution, and it is such a serious defect that we want to be able to catch it. The general mechanism is to replace the disparate (but properly ordered) direct clinit calls of the generic ClassInfo.initializeClass() with a single sythetic method that includes all required locking (bottom up), clinit calls / class status change (top down), and unlocking (top down). We also need to add a synthetic insn to defer changing the class status of classes that don't have clinits(), or otherwise the correct lock/unlock order will not amount to anything if the hierarchy is entered through one of the clinit-absent classes. Now we get proper deadlocks if there are concurrent cyclic dependencies during class resolution. However, this can be such a state exploder that we certainly don't want this as the default behavior, especially since it probably is hotspot specific. Nested class init locking is therefore controlled by jvm.nested_init and respective jvm.nested_init.include/exclude options. Added a NestedInitTest to demonstrate use. Thanks to Lilia Abdulina for bringing this long forgotten issue up Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	314
0 61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	315 ############################### 3. CG part ###############################
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	316
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	317 # choice randomization policy in effect:
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	318 # "NONE" - choice sets are not randomized
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	319 # "FIXED_SEED" - choice sets are randomized using a fixed seed for each JPF run (reproducible)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	320 # "VAR_SEED" - choice sets are randomized using a variable seed for each JPF run
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	321 cg.randomize_choices = NONE
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	322
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	323 # the standard seed value used for the FIXED_SEED policy
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	324 cg.seed = 42
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	325
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	326
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	327 # if this is set, we create choice generators even if there is only a single
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	328 # choice. This is to ensure state storage/matching at all locations where a
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	329 # choice generator could be created. The default should be to turn it off though,
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	330 # since this can produce a lot of additional states (esp. with threads)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	331 cg.break_single_choice = false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	332
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	333
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	334 # default BooleanChoiceGenerator sequence: do we start with 'false'
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	335 cg.boolean.false_first = true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	336
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	337 # do we want java.util.Random. nextXX() enumerate choices, or just return a single value?
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	338 # (isn't implemented for all types yet)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	339 cg.enumerate_random=false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	340
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	341 # maximum number of processors returned by Runtime.availableProcessors(). If this is
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	342 # greater than 1, the call represents a ChoiceGenerator
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	343 cg.max_processors=1
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	344
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	345 # creates a CG upon Thread.start, i.e. breaks the starting transition. Note this is
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	346 # required for data race detection (which depends on detecting access of shared objects)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	347 cg.threads.break_start=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	348
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	349 # if this option is set we break the transition on Thread.yield()
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	350 cg.threads.break_yield=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	351
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	352 # if this option is set we break the transition on Thread.sleep()
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	353 cg.threads.break_sleep=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	354
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	355 # set if we shold also break on array instructions, e.g. to detect races
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	356 # for array elements. This is off by default because it can cause serious
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	357 # state explosion
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	358 cg.threads.break_arrays=false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	359
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	360 # do we support atomic sections. If set to false, Verify.beginAtomic()/endAtomic()
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	361 # will not do anything
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	362 cg.enable_atomic=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	363
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	364 ############################### 3. Report Part ###############################
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	365 log.handler.class=gov.nasa.jpf.util.LogHandler
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	366
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	367 # Windows seem to have a different default
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	368 log.level=warning
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	369
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	370 report.class=gov.nasa.jpf.report.Reporter
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	371 report.publisher=console
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	372
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	373 report.console.class=gov.nasa.jpf.report.ConsolePublisher
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	374
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	375 # this prints out repository information if the 'jpf' topic is set (for debugging)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	376 #jpf.report.show_repository=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	377
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	378 #property violation reporting is configured separately
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	379 report.console.start=jpf,sut
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	380
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	381 report.console.transition=
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	382 report.console.constraint=constraint,snapshot
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	383
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	384 report.console.probe=statistics
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	385
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	386 report.console.property_violation=error,snapshot
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	387 report.console.show_steps=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	388 report.console.show_method=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	389 report.console.show_code=false
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	390
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	391 report.console.finished=result,statistics
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	392
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	393 #jpf.report.console.show_steps=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	394 #jpf.report.console.show_method=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	395 #jpf.report.console.show_code=true
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	396
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	397 report.xml.class=gov.nasa.jpf.report.XMLPublisher
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	398
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	399 report.html.class=gov.nasa.jpf.report.HTMLPublisher
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	400 report.html.start=jpf,sut,platform,user,dtg,config
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	401 report.html.constraint=constraint
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	402 report.html.property_violation=
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	403 report.html.finished=result,statistics,error,snapshot,output
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	404
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	405
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	406 ############################### 4. Listener part #############################
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	407
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	408 # imperative list of listeners
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	409 #listener=
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	410
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	411 listener.autoload=\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	412 gov.nasa.jpf.NonNull,\
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	413 gov.nasa.jpf.Const
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	414
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	415 listener.gov.nasa.jpf.NonNull=gov.nasa.jpf.tools.NonNullChecker
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	416 listener.gov.nasa.jpf.Const=gov.nasa.jpf.tools.ConstChecker
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	417
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	418
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	419 ### PreciseRaceDetector
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	420
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	421 # we don't check for races in standard libraries
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	422 race.exclude=java.,javax.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	423
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	424
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	425 ############################### 5. test part #############################
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	426
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	427 test.report.console.finished=result

Mercurial > hg > Members > kono > jpf-core

annotate jpf.properties @ 34:49be04cc6389 default tip java9-try