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