Go to the documentation of this file.
9 #ifndef CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H
10 #define CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H
12 #define COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth"
13 #define COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \
14 "max-nondet-tree-depth"
15 #define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size"
16 #define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size"
17 #define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \
18 "function-pointer-can-be-null"
19 #define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "havoc-member"
22 #define COMMON_HARNESS_GENERATOR_OPTIONS \
23 "(" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):" \
24 "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \
25 "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \
26 "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \
27 "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT "):" \
28 "(" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "):" \
29 // COMMON_HARNESS_GENERATOR_OPTIONS
34 #define COMMON_HARNESS_GENERATOR_HELP \
35 "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT \
36 " N minimum level at which a pointer can first be NULL\n" \
37 " in a recursively nondet initialized struct\n" \
38 "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \
39 " N limit size of nondet (e.g. input) object tree;\n" \
40 " at level N pointers are set to null\n" \
41 "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT \
42 " N minimum size of dynamically created arrays\n" \
44 "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \
45 " N maximum size of dynamically created arrays\n" \
47 "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \
48 " <function-name>, name of the function(s) pointer parameters\n" \
49 " that can be NULL pointing.\n" \
50 "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT \
51 " <member-expr> path to the member to be havoced\n" \
52 // COMMON_HARNESS_GENERATOR_HELP
56 #endif // CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H