CBMC
common_harness_generator_options.h
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: common_harness_generator_options
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
9 #ifndef CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H
10 #define CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H
11 
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"
20 
21 // clang-format off
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
30 
31 // clang-format on
32 
33 // clang-format off
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" \
43  " (default: 1)\n" \
44  "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \
45  " N maximum size of dynamically created arrays\n" \
46  " (default: 2)\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
53 
54 // clang-format on
55 
56 #endif // CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H