CBMC
memory_snapshot_harness_generator_options.h File Reference
+ Include dependency graph for memory_snapshot_harness_generator_options.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT   "memory-snapshot"
 
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT   "initial-goto-location"
 
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT   "initial-source-location"
 
#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT   "havoc-variables"
 
#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT   "pointer-as-array"
 
#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT   "size-of-array"
 
#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS
 
#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
 

Macro Definition Documentation

◆ MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT

#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT   "size-of-array"

Definition at line 19 of file memory_snapshot_harness_generator_options.h.

◆ MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP

#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
Value:
"memory snapshot harness generator ({y--harness-type}\n" \
" {yinitialize-with-memory-snapshot}):\n" \
"} {ufile} \t " \
"initialize memory from JSON memory snapshot\n" \
"} {ufunc}[{y:}{un}] " \
"\t " \
"use given function and location number as entry point\n" \
"} {ufile}{y:}{un} " \
"\t " \
"use given file name and line number as entry point\n" \
"} {uvars} \t " \
"initialize variables from {uvars} to non-deterministic " \
"} {up} \t " \
"treat the global pointer with the name {up} as an array\n" \
"} " \
"{uarray_name}{y:}{usize_name} \t " \
"set the parameter {usize_name} to the size of the array {uarray_name} " \
"(implies " \
"} " \
"{uarray_name})\n"
#define COMMON_HARNESS_GENERATOR_HELP
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT
#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT
#define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT
#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT
#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT
#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT

Definition at line 34 of file memory_snapshot_harness_generator_options.h.

◆ MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS

◆ MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT

#define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT   "havoc-variables"

Definition at line 17 of file memory_snapshot_harness_generator_options.h.

◆ MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT

#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT   "initial-goto-location"

Definition at line 15 of file memory_snapshot_harness_generator_options.h.

◆ MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT

#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT   "initial-source-location"

Definition at line 16 of file memory_snapshot_harness_generator_options.h.

◆ MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT

#define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT   "memory-snapshot"

Definition at line 14 of file memory_snapshot_harness_generator_options.h.

◆ MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT

#define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT   "pointer-as-array"

Definition at line 18 of file memory_snapshot_harness_generator_options.h.