cprover
Loading...
Searching...
No Matches
memory_snapshot_harness_generator_options.h
Go to the documentation of this file.
1/******************************************************************\
2
3Module: memory_snapshot_harness_generator_options
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
9#ifndef CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H
10#define CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H
11
13
14#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "memory-snapshot"
15#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT "initial-goto-location"
16#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT "initial-source-location"
17#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "havoc-variables"
18#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "pointer-as-array"
19#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "size-of-array"
20
21// clang-format off
22#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \
23 "(" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "):" \
24 "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT "):" \
25 "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT "):" \
26 "(" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "):" \
27 "(" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "):" \
28 "(" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "):" \
29// MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS
30
31// clang-format on
32
33// clang-format off
34#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP \
35 "memory snapshot harness generator (--harness-type\n" \
36 " initialise-from-memory-snapshot)\n\n" \
37 "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " <file> initialise memory " \
38 "from JSON memory snapshot\n" \
39 "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " <func[:<n>]>\n" \
40 " use given function and location number as " \
41 "entry\n point\n" \
42 "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT " <file:<n>>\n" \
43 " use given file name and line number as " \
44 "entry\n point\n" \
45 "--" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT " vars initialise" \
46 " variables from `vars' to\n" \
47 " non-deterministic values\n" \
48 COMMON_HARNESS_GENERATOR_HELP \
49 "--" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \
50 " p treat the global pointer with the name `p' as\n" \
51 " an array\n" \
52 "--" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT \
53 " array_name:size_name\n" \
54 " set the parameter <size_name> to the size" \
55 " of\n the array <array_name>\n" \
56 " (implies " \
57 "-- " MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT \
58 " <array_name>)\n" \
59// MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
60
61// clang-format on
62
63#endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS_H