cprover
Loading...
Searching...
No Matches
function_harness_generator_options.h
Go to the documentation of this file.
1/******************************************************************\
2
3Module: functions_harness_generator_options
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
9#ifndef CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
10#define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
11
13
14#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function"
15#define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT "nondet-globals"
16#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \
17 "treat-pointer-as-array"
18#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \
19 "treat-pointers-equal"
20#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \
21 "associated-array-size"
22#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \
23 "treat-pointer-as-cstring"
24#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT \
25 "treat-pointers-equal-maybe"
26
27// clang-format off
28#define FUNCTION_HARNESS_GENERATOR_OPTIONS \
29 "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \
30 "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")" \
31 "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):" \
32 "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT "):" \
33 "(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):" \
34 "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING "):" \
35 "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT ")" \
36// FUNCTION_HARNESS_GENERATOR_OPTIONS
37
38// clang-format on
39
40// clang-format off
41#define FUNCTION_HARNESS_GENERATOR_HELP \
42 "function harness generator (--harness-type call-function)\n\n" \
43 "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT \
44 " the function the harness should call\n" \
45 "--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT \
46 " set global variables to non-deterministic values\n" \
47 " in harness\n" \
48 COMMON_HARNESS_GENERATOR_HELP \
49 "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \
50 " p treat the function parameter with the name `p' as\n" \
51 " an array\n" \
52 "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT \
53 " p,q,r[;s,t] treat the function parameters `q,r' equal\n" \
54 " to parameter `p'; `s` to `t` and so on\n" \
55 "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT \
56 " function parameters equality is non-deterministic\n" \
57 "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \
58 " array_name:size_name\n" \
59 " set the parameter <size_name> to the size" \
60 " of\n the array <array_name>\n" \
61 " (implies " \
62 "-- " FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \
63 " <array_name>)\n" \
64 "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \
65 " p treat the function parameter with the name `p' as\n" \
66 " a string of characters\n" \
67 // FUNCTION_HARNESS_GENERATOR_HELP
68
69// clang-format on
70
71#endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H