### Setup Commands for SMT2 Parser

Source: https://diffblue.github.io/cbmc/smt2__solver_8cpp_source.html

Sets up the command handlers for the SMT2 parser. This example shows the setup for the 'assert' command, which parses an expression and adds it to the solver if it's not nil.

```cpp
void smt2_solvert::setup_commands()
{
 {
 commands["assert"] = [this]() {
 exprt e = expression();
 if(e.is_not_nil())
 {

```

--------------------------------

### Proof Harness Example

Source: https://diffblue.github.io/cbmc/contracts-assigns.html

Illustrates a basic proof harness setup using C. This includes memory allocation and clearing for a vector structure.

```c
// Proof harness
int main() {
size_t size;
struct vec_t *vec = vec_alloc(size);
vec_clear(vec);
}
```

--------------------------------

### __builtin_GOMP_loop_guided_start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Starts a guided loop in OpenMP.

```APIDOC
## __builtin_GOMP_loop_guided_start

### Description
Starts a guided loop in OpenMP.

### Signature
_Bool __builtin_GOMP_loop_guided_start(long, long, long, long, long*, long*);
```

--------------------------------

### __builtin_GOMP_loop_ordered_guided_start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Starts an ordered guided loop in OpenMP.

```APIDOC
## __builtin_GOMP_loop_ordered_guided_start

### Description
Starts an ordered guided loop in OpenMP.

### Signature
_Bool __builtin_GOMP_loop_ordered_guided_start(long, long, long, long, long*, long*);
```

--------------------------------

### set_up_custom_entry_point

Source: https://diffblue.github.io/cbmc/initialize__goto__model_8cpp.html

Prepares a custom entry point to replace `__CPROVER_start` based on the 'function' option.

```APIDOC
## set_up_custom_entry_point()

### Description
Process the "function" option in `options` to prepare a custom entry point to replace `__CPROVER_start`.

### Parameters
* `_language_files_` (language_filest &) - Language parsing and type checking facilities.
* `_symbol_table_` (symbol_tablet &) - Symbol table for mode lookup and removal of an existing entry point.
* `_unload_` (const std::function<std::size_t(const irep_idt &)> &) - Functor to remove an existing entry point.
* `_options_` (const optionst &) - Configuration options.
* `_try_mode_lookup_` (bool) - Try to infer the entry point's mode from the symbol table.
* `_message_handler_` (message_handlert &) - Message handler.
```

--------------------------------

### OpenMP Loop Doacross Guided Start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Starts a doacross loop with guided scheduling.

```APIDOC
## __builtin_GOMP_loop_ull_doacross_guided_start

### Description
Initiates a doacross loop construct with guided scheduling for unsigned long long loop variables. Chunk sizes are adjusted dynamically.

### Method
`_Bool __builtin_GOMP_loop_ull_doacross_guided_start(unsigned, unsigned long long *, unsigned long long, unsigned long long *, unsigned long long *)`

### Parameters
- `unsigned` - Loop identifier.
- `unsigned long long *` - Pointer to the current iteration.
- `unsigned long long` - End of the loop.
- `unsigned long long *` - Pointer to the last iteration.
- `unsigned long long *` - Pointer to the step.
```

--------------------------------

### Get Reachable Class Identifiers

Source: https://diffblue.github.io/cbmc/class__hierarchy_8cpp_source.html

Gets all reachable class identifiers from a starting class, either forwards (children) or backwards (parents). It removes the starting class itself from the result. Note: The TODO suggests a more direct approach might be beneficial.

```cpp
class_hierarchy_grapht::idst class_hierarchy_grapht::get_other_reachable_ids(
 const irep_idt &c,
 bool forwards) const
{
 idst direct_child_ids;
 const node_indext &node_index = nodes_by_name.at(c);
 const auto &reachable_indices = get_reachable(node_index, forwards);
 auto reachable_ids = ids_from_indices(reachable_indices);
 // Remove c itself from the list
 // TODO Adding it first and then removing it is not ideal. It would be
 // better to define a function grapht::get_other_reachable and directly use
 // that here.
 reachable_ids.erase(
 std::remove(reachable_ids.begin(), reachable_ids.end(), c),
 reachable_ids.end());
 return reachable_ids;
}
```

--------------------------------

### setup_commands()

Source: https://diffblue.github.io/cbmc/classsmt2__solvert.html

Sets up the commands for the SMT2 solver.

```APIDOC
## void setup_commands()

### Description
Sets up the commands for the SMT2 solver.

### Method
void protected
```

--------------------------------

### OpenMP Loop Ull Nonmonotonic Guided Start Function

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Starts an OpenMP loop with unsigned long long iterators using nonmonotonic guided scheduling. This scheduling policy adjusts chunk sizes dynamically based on workload.

```c
_Bool __builtin_GOMP_loop_ull_nonmonotonic_guided_start(_Bool, unsigned long long, unsigned long long, unsigned long long, unsigned long long, unsigned long long *, unsigned long long *);
```

--------------------------------

### set_up_custom_entry_point

Source: https://diffblue.github.io/cbmc/initialize__goto__model_8h_source.html

Sets up a custom entry point, potentially replacing __CPROVER_start, based on options.

```APIDOC
## set_up_custom_entry_point

### Description
Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.

### Signature
void set_up_custom_entry_point(
 language_filest &language_files,
 symbol_tablet &symbol_table,
 const std::function<std::size_t(const irep_idt &)> &unload,
 const optionst &options,
 bool try_mode_lookup,
 message_handlert &message_handler
);
```

--------------------------------

### setup

Source: https://diffblue.github.io/cbmc/qbf__squolem__core_8cpp_source.html

Configures the Squolem solver with various options.

```APIDOC
## void setup(void)

### Description
Sets up the Squolem solver by clearing existing quantifiers and clauses, initializing the internal Squolem object, and configuring its options such as debug file output and model compression.

### Method
void

### Parameters
None

### Request Example
```cpp
qbf_squolem_coret solver;
solver.setup();
```

### Response
Configures the solver instance.
```

--------------------------------

### Example XML for Options

Source: https://diffblue.github.io/cbmc/xml__interface_8cpp.html

An example of XML structure used to define command-line options, including value options and flag options with their respective names and actual values.

```xml
<options>
<valueOption actual="main.c"/>
<valueOption name="function" actual="foo"/>
<valueOption name="unwind" actual="3"/>
<valueOption name="property" actual="foo.assertion.1"/>
<valueOption name="property" actual="foo.assertion.3"/>
<flagOption name="trace" actual="on"/>
<flagOption name="show-properties" actual="off"/>
</options>
```

--------------------------------

### __builtin_GOMP_loop_nonmonotonic_guided_start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Starts a non-monotonic guided loop in OpenMP.

```APIDOC
## __builtin_GOMP_loop_nonmonotonic_guided_start

### Description
Starts a non-monotonic guided loop in OpenMP.

### Signature
_Bool __builtin_GOMP_loop_nonmonotonic_guided_start(long, long, long, long, long*, long*);
```

--------------------------------

### Construction and Setup

Source: https://diffblue.github.io/cbmc/classcfg__baset_1_1entry__mapt-members.html

Constructors and methods for initializing the entry_mapt.

```APIDOC
## Construction and Setup

### Description
Constructors and methods for initializing and setting up the `entry_mapt`.

### Methods
- `entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)`: Constructor that takes a reference to the containing graph.
- `setup_for_keys(Iter begin, Iter end)`: Sets up the map for a given range of keys.
```

--------------------------------

### __builtin_GOMP_loop_doacross_guided_start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h.html

Starts a guided OpenMP doacross loop.

```APIDOC
## Function: __builtin_GOMP_loop_doacross_guided_start

### Description
Initiates a guided OpenMP doacross loop, where the chunk size for iterations decreases over time.

### Signature
`_Bool __builtin_GOMP_loop_doacross_guided_start(unsigned, long *, long, long *, long *);`
```

--------------------------------

### __builtin_GOMP_loop_guided_next

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Gets the next iteration for a guided loop in OpenMP.

```APIDOC
## __builtin_GOMP_loop_guided_next

### Description
Gets the next iteration for a guided loop in OpenMP.

### Signature
_Bool __builtin_GOMP_loop_guided_next(long*, long*);
```

--------------------------------

### main

Source: https://diffblue.github.io/cbmc/classcw__modet.html

Starts the compiler with the provided command-line arguments.

```APIDOC
## main

### Description
Starts the compiler.

### Method
int

### Parameters
- **argc** (int) - The number of command-line arguments.
- **argv** (const char**) - An array of command-line argument strings.

### Response
- **int**: Return value indicating the exit status of the compiler.
```

--------------------------------

### qbf_squolem_coret::setup

Source: https://diffblue.github.io/cbmc/qbf__squolem__core_8cpp_source.html

Initializes or sets up the QBF solver environment. This is typically called before performing any solving operations.

```APIDOC
## qbf_squolem_coret::setup

### Description
Sets up the QBF solver environment.

### Signature
void setup(void)
```

--------------------------------

### Get Archive File Start Offset

Source: https://diffblue.github.io/cbmc/miniz_8cpp.html

Retrieves the starting offset of the zip archive's file data within the archive stream or file.

```APIDOC
## mz_zip_get_archive_file_start_offset

### Description
Returns the starting offset of the archive's file data.

### Signature
mz_uint64 mz_zip_get_archive_file_start_offset(mz_zip_archive *pZip)

### Parameters
- **pZip** (*mz_zip_archive*): Pointer to the zip archive structure.

### Returns
- **mz_uint64**: The starting offset of the file data.
```

--------------------------------

### main()

Source: https://diffblue.github.io/cbmc/classms__link__modet.html

Starts the compiler.

```APIDOC
## int main(int argc, const char **argv)

### Description
starts the compiler

### Method
`int`

### Parameters
* **argc** (int) - The number of command-line arguments.
* **argv** (const char **) - An array of command-line argument strings.
```

--------------------------------

### mz_zip_get_archive_file_start_offset

Source: https://diffblue.github.io/cbmc/miniz_8h_source.html

Gets the starting offset of the first file in the zip archive.

```APIDOC
## mz_zip_get_archive_file_start_offset

### Description
Retrieves the byte offset within the archive where the data for the first file begins.

### Signature
```c
MINIZ_EXPORT mz_uint64 mz_zip_get_archive_file_start_offset(mz_zip_archive *pZip)
```

### Parameters
*   **pZip** (mz_zip_archive *) - A pointer to the zip archive structure.

### Returns
Returns the starting offset of the first file as a `mz_uint64`.
```

--------------------------------

### __builtin_GOMP_loop_ordered_guided_next

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Gets the next iteration for an ordered guided loop in OpenMP.

```APIDOC
## __builtin_GOMP_loop_ordered_guided_next

### Description
Gets the next iteration for an ordered guided loop in OpenMP.

### Signature
_Bool __builtin_GOMP_loop_ordered_guided_next(long*, long*);
```

--------------------------------

### Setup QBF Squolem Core

Source: https://diffblue.github.io/cbmc/qbf__squolem__core_8cpp_source.html

Initializes the QBF Squolem Core solver. This function should be called before using other methods of the class.

```cpp
void setup(void)
**Definition** qbf_squolem_core.cpp:26
```

--------------------------------

### setup_for_keys()

Source: https://diffblue.github.io/cbmc/classdense__integer__mapt.html

Initializes the map with a set of allowed keys.

```APIDOC
## setup_for_keys()

### Description
Sets the keys that are allowed to be used in this container. This function should be called before the container is used. It checks that the integers produced for each key by `KeyToDenseInteger` are unique and fall within a `std::size_t`'s range. Using keys not provided to this function with `operator[]`, `insert`, `at(...)` etc. may cause an invariant failure or undefined behavior.

### Signature
```cpp
template<class K , class V , class KeyToDenseInteger = identity_functort>
template<typename Iter >
void dense_integer_mapt< K, V, KeyToDenseInteger >::setup_for_keys(Iter _first, Iter _last)
```

### Parameters
* **_first** (Iter) - An iterator to the beginning of the range of keys.
* **_last** (Iter) - An iterator to the end of the range of keys.
```

--------------------------------

### Get Archive File Start Offset - C

Source: https://diffblue.github.io/cbmc/miniz_8cpp_source.html

Returns the starting offset of the archive's file data within the archive. Returns 0 if the archive or its state is invalid.

```c
mz_uint64 mz_zip_get_archive_file_start_offset(mz_zip_archive *pZip)
{
 if ((!pZip) || (!pZip->m_pState))
 return 0;
 return pZip->m_pState->m_file_archive_start_ofs;
}
```

--------------------------------

### Set Up Custom Entry Point C++

Source: https://diffblue.github.io/cbmc/initialize__goto__model_8cpp_source.html

Configures a custom entry point for the goto program, potentially rebuilding the start function if binaries are provided and a specific function is requested.

```cpp
void set_up_custom_entry_point(
    language_filest &language_files,
    symbol_tablet &symbol_table,
    const std::function<std::size_t(const irep_idt &)> &unload,
    const optionst &options,
    bool try_mode_lookup,
    message_handlert &message_handler)
{
 bool binaries_provided_start =
 symbol_table.has_symbol(goto_functionst::entry_point());

 bool entry_point_generation_failed=false;

 if(binaries_provided_start && options.is_set("function"))
 {
 // The goto binaries provided already contain a __CPROVER_start
 // function that may be tied to a different entry point `function`.
 // Hence, we will rebuild the __CPROVER_start function.

 // Get the language annotation of the existing __CPROVER_start function.
 std::unique_ptr<languaget> language =
 get_entry_point_language(symbol_table, options, message_handler);

```

--------------------------------

### main()

Source: https://diffblue.github.io/cbmc/classarmcc__modet.html

Starts the compiler process.

```APIDOC
## main(int argc, const char **argv)

### Description
Initializes and starts the compiler process with the given command-line arguments.

### Parameters
*   **argc** (int) - The number of command-line arguments.
*   **argv** (const char **) - An array of command-line argument strings.

### Returns
An integer representing the exit status of the compiler.
```

--------------------------------

### __builtin_GOMP_loop_ull_ordered_guided_start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h.html

Starts a loop iteration for unsigned long long with guided ordered scheduling.

```APIDOC
## __builtin_GOMP_loop_ull_ordered_guided_start()

### Description
Initiates a loop iteration for unsigned long long with guided ordered scheduling.

### Signature
_Bool __builtin_GOMP_loop_ull_ordered_guided_start( _Bool, unsigned long long, unsigned long long, unsigned long long, unsigned long long, unsigned long long *, unsigned long long * )
```

--------------------------------

### String Solver Example

Source: https://diffblue.github.io/cbmc/group__solvers.html

This example demonstrates how to use the string solver for string logic operations. It shows the setup of constraints for string concatenation and equality checks, and the expected satisfiable outcome.

```c
return_code == cprover_string_concat_func(
length1, array1,
{ .length=length2, .content=content2 },
{ .length=length3, .content=content3 })
length3 == length2
content3 == content2
is_equal == cprover_string_equals_func(length1, array1, 2, {'a', 'a'})
is_equal == 1
```

--------------------------------

### help()

Source: https://diffblue.github.io/cbmc/classgoto__harness__parse__optionst-members.html

Displays help information for the goto harness parsing options.

```APIDOC
## help()

### Description
Overrides the base class method to display detailed help messages related to goto harness command-line options.

### Method
virtual
```

--------------------------------

### Add --greet switch to goto-instrument

Source: https://diffblue.github.io/cbmc/tutorial.html

This example demonstrates how to add a new command-line switch '--greet' that takes an optional argument. The switch prints a greeting message, optionally including a provided name. Ensure the option is added to the header file and returns 0 after execution.

```bash
$ goto-instrument --greet main.gb
hello, world!
$ goto-instrument --greet Leperina main
hello, Leperina!
```

--------------------------------

### Get Abstract Traces Before Instruction - ai_baset

Source: https://diffblue.github.io/cbmc/ai_8h_source.html

Returns all histories that have reached the start of a given instruction.

```cpp
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const

```

--------------------------------

### help()

Source: https://diffblue.github.io/cbmc/classgoto__analyzer__parse__optionst.html

Displays command-line help information for the goto analyzer.

```APIDOC
## void help()

### Description
Displays detailed command-line help information to the user, explaining available options and usage for the goto analyzer. This method overrides a virtual function from the base class.

### Returns
None.
```

--------------------------------

### __builtin_GOMP_loop_ull_nonmonotonic_guided_start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Starts an OpenMP loop with unsigned long long bounds and guided, non-monotonic scheduling.

```APIDOC
## __builtin_GOMP_loop_ull_nonmonotonic_guided_start

### Description
Starts an OpenMP loop with unsigned long long bounds and guided, non-monotonic scheduling.

### Signature
_Bool __builtin_GOMP_loop_ull_nonmonotonic_guided_start(_Bool, unsigned long long, unsigned long long, unsigned long long, unsigned long long, unsigned long long *, unsigned long long *);
```

--------------------------------

### setup_for_keys

Source: https://diffblue.github.io/cbmc/classcfg__baset_1_1entry__mapt.html

Sets up the entry_mapt for a range of keys, typically used for initialization.

```APIDOC
## setup_for_keys(Iter begin, Iter end)

### Description
Initializes or prepares the entry_mapt to handle keys within the specified range.

### Signature
```cpp
template<class Iter>
void setup_for_keys(Iter begin, Iter end)
```

### Parameters
*   **begin** (Iter) - An iterator pointing to the beginning of the key range.
*   **end** (Iter) - An iterator pointing to the end of the key range.
```

--------------------------------

### __builtin_GOMP_loop_ull_ordered_guided_next

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h.html

Gets the next iteration for an unsigned long long loop with guided ordered scheduling.

```APIDOC
## __builtin_GOMP_loop_ull_ordered_guided_next()

### Description
Retrieves the next iteration for an unsigned long long loop using guided ordered scheduling.

### Signature
_Bool __builtin_GOMP_loop_ull_ordered_guided_next( unsigned long long *, unsigned long long * )
```

--------------------------------

### setup_commands

Source: https://diffblue.github.io/cbmc/classsmt2__parsert.html

Initializes the command processing logic. This is a protected method.

```APIDOC
## setup_commands()

### Signature
`void smt2_parsert::setup_commands()`

### Description
Configures the parser to handle SMT2 commands.

### Definition
`smt2_parser.cpp:1678`
```

--------------------------------

### __builtin_GOMP_loop_ull_guided_next

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Gets the next iteration for a loop with unsigned long long indices and guided scheduling. Used in OpenMP.

```APIDOC
## __builtin_GOMP_loop_ull_guided_next

### Description
Retrieves the next iteration for a loop using unsigned long long indices with a guided scheduling policy.

### Parameters
* `unsigned long long *`: Pointer to store the current iteration number.
* `unsigned long long *`: Pointer to store the iteration step.
```

--------------------------------

### Get Recursive Aliased Objects

Source: https://diffblue.github.io/cbmc/local__may__alias_8h_source.html

Recursively collects objects that are aliased by the given expression, starting from a source location information.

```cpp
void get_rec(
 object_sett &dest,
 const exprt &rhs,
 const loc_infot &loc_info_src) const;
```

--------------------------------

### Initialize Symbolic Execution from Entry Point

Source: https://diffblue.github.io/cbmc/symex__bmc__incremental__one__loop_8cpp_source.html

Sets up the initial state for symbolic execution and performs the execution using the provided goto function. Returns a boolean indicating whether to pause the symbolic execution.

```cpp
125bool symex_bmc_incremental_one_loopt::from_entry_point_of(
126 const get_goto_functiont &get_goto_function,
127 symbol_tablet &new_symbol_table)
128{
129 state = initialize_entry_point_state(get_goto_function);
130
131 new_symbol_table = symex_with_state(*state, get_goto_function);
132
133 return should_pause_symex;
134}
```

--------------------------------

### make_entry()

Source: https://diffblue.github.io/cbmc/classdep__graph__domaint.html

Initializes the domain to a reasonable entry-point state.

```APIDOC
## make_entry()

### Description
Initializes the domain to a reasonable entry-point state. For most domains, this is the top state.

### Signature
`void dep_graph_domaint::make_entry()`
```

--------------------------------

### __builtin_GOMP_loop_ull_guided_start

Source: https://diffblue.github.io/cbmc/gcc__builtin__headers__omp_8h_source.html

Starts a loop with unsigned long long indices and guided scheduling. Used in OpenMP for dynamic iteration distribution.

```APIDOC
## __builtin_GOMP_loop_ull_guided_start

### Description
Initiates a loop with unsigned long long indices and a guided scheduling policy. Iterations are distributed dynamically with decreasing chunk sizes.

### Parameters
* `_Bool`: Flag for guided scheduling.
* `unsigned long long`: The starting iteration.
* `unsigned long long`: The ending iteration.
* `unsigned long long`: The initial chunk size.
* `unsigned long long`: The stride.
* `unsigned long long *`: Pointer to store the current iteration.
* `unsigned long long *`: Pointer to store the iteration step.
```

--------------------------------

### initialize [2/2]

Source: https://diffblue.github.io/cbmc/classflow__insensitive__analysis__baset.html

Initializes the analysis with a goto program. This is an inline virtual method.

```APIDOC
## initialize() [2/2]

### Description
Initializes the analysis with a goto program.

### Signature
`virtual void flow_insensitive_analysis_baset::initialize(const goto_programt &)`

### Modifiers
inline virtual

### Reimplementation Notes
Reimplemented in `value_set_analysis_fit`.

### Definition
`flow_insensitive_analysis.h`, line 111
```

--------------------------------

### Get Reachable Nodes (Multiple Sources)

Source: https://diffblue.github.io/cbmc/classcall__grapht_1_1directed__grapht.html

Performs a Depth-First Search starting from multiple source nodes and returns a list of all reachable nodes.

```APIDOC
## get_reachable (multiple sources)

### Description
Run depth-first search on the graph, starting from multiple source nodes.

### Signature
std::vector<node_indext> get_reachable(const std::vector<node_indext> &src, bool forwards) const

### Parameters
* **src** (const std::vector<node_indext> &) - A vector of source node indices.
* **forwards** (bool) - If true, search in the forward direction; otherwise, search in the backward direction.

### Returns
std::vector<node_indext> - A vector of node indices that are reachable from the source nodes.
```

--------------------------------

### help()

Source: https://diffblue.github.io/cbmc/classarmcc__modet.html

Displays general command-line help.

```APIDOC
## help()

### Description
Displays general command-line help information.

### Method
void
```

--------------------------------

### Get Reachable Nodes (Single Source)

Source: https://diffblue.github.io/cbmc/classcall__grapht_1_1directed__grapht.html

Performs a Depth-First Search starting from a single source node and returns a list of all reachable nodes.

```APIDOC
## get_reachable (single source)

### Description
Run depth-first search on the graph, starting from a single source node.

### Signature
std::vector<node_indext> get_reachable(node_indext src, bool forwards) const

### Parameters
* **src** (node_indext) - The index of the source node.
* **forwards** (bool) - If true, search in the forward direction; otherwise, search in the backward direction.

### Returns
std::vector<node_indext> - A vector of node indices that are reachable from the source node.
```

--------------------------------

### Get Configuration

Source: https://diffblue.github.io/cbmc/variable__sensitivity__object__factory_8h_source.html

Returns a constant reference to the configuration object used by the factory.

```cpp
const vsd_configt &config() const
{
  return configuration;
}
```

--------------------------------

### Get expression recursively

Source: https://diffblue.github.io/cbmc/boolbv__get_8cpp_source.html

Recursively retrieves an expression from a bit-vector starting at a specific offset. This is a core function for deconstructing bit-vectors into their expression components.

```cpp
exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const
{
  return result;
}
```

--------------------------------

### Initialize from Source Files C++

Source: https://diffblue.github.io/cbmc/initialize__goto__model_8cpp_source.html

Parses a list of source files, converts them to a goto program, and typechecks them. Throws exceptions for file opening or parsing errors.

```cpp
void initialize_from_source_files(
    const std::list<std::string> &sources,
    const optionst &options,
    language_filest &language_files,
    symbol_tablet &symbol_table,
    message_handlert &message_handler)
{
 if(sources.empty())
 return;

 messaget msg(message_handler);

 for(const auto &filename : sources)
 {
 std::ifstream infile(widen_if_needed(filename));

 if(!infile)
 {
 throw system_exceptiont("Failed to open input file '" + filename + '\'');
 }

 language_filet &lf = language_files.add_file(filename);
 lf.language = get_language_from_filename(filename);

 if(lf.language == nullptr)
 {
 throw invalid_command_line_argument_exceptiont{
 "Failed to figure out type of file", filename};
 }

 languaget &language = *lf.language;
 language.set_language_options(options, message_handler);

 msg.progress() << "Parsing " << filename << messaget::eom;

 if(language.parse(infile, filename, message_handler))
 {
 throw invalid_input_exceptiont("PARSING ERROR");
 }

 lf.get_modules();
 }

 msg.progress() << "Converting" << messaget::eom;

 if(language_files.typecheck(symbol_table, message_handler))
 {
 throw invalid_input_exceptiont("CONVERSION ERROR");
 }
}
```

--------------------------------

### setup_symex(symex_bmct & _symex_)

Source: https://diffblue.github.io/cbmc/classjava__single__path__symex__checkert.html

Sets up the symbolic execution for the checker.

```APIDOC
## setup_symex(symex_bmct & _symex_)

### Description
Configures and initializes the symbolic execution engine with the provided `symex_bmct` instance.

### Method
`void java_single_path_symex_checkert::setup_symex(symex_bmct & _symex_)`

### Parameters
* **_symex_** (`symex_bmct &`) - The symbolic execution engine to set up.
```

--------------------------------

### Get Function Preconditions

Source: https://diffblue.github.io/cbmc/instrument__preconditions_8cpp_source.html

Retrieves all assert statements marked as preconditions at the beginning of a function's body. Assumes preconditions are contiguous at the start of the function.

```cpp
std::vector<goto_programt::const_targett> get_preconditions(
 const symbol_exprt &function,
 const goto_functionst &goto_functions)
{
 const irep_idt &identifier = function.identifier();

 auto f_it=goto_functions.function_map.find(identifier);
 if(f_it==goto_functions.function_map.end())
 return {};

 const auto &body=f_it->second.body;

 std::vector<goto_programt::const_targett> result;

 for(auto i_it=body.instructions.begin();
 i_it!=body.instructions.end();
 i_it++)
 {
 if(i_it->is_location() ||
 i_it->is_skip())
 continue; // ignore

 if(
 i_it->is_assert() &&
 i_it->source_location().get_property_class() == ID_precondition)
 {
 result.push_back(i_it);
 }
 else
 break; // preconditions must be at the front
 }

 return result;
}
```

--------------------------------

### java_setup_symex

Source: https://diffblue.github.io/cbmc/java__bmc__util_8h.html

Registers Java-specific preprocessing handlers with goto-symex.

```APIDOC
## java_setup_symex()

### Description
Registers Java-specific preprocessing handlers with goto-symex.

### Signature
void java_setup_symex(const optionst &options, abstract_goto_modelt &goto_model, symex_bmct &symex)

### Parameters
- **options**: const optionst &
- **goto_model**: abstract_goto_modelt &
- **symex**: symex_bmct &

### Definition
Defined in file java_bmc_util.h, line 18 of java_bmc_util.cpp.
```

--------------------------------

### Main Function Example

Source: https://diffblue.github.io/cbmc/contracts-function-pointer-predicates.html

A simple main function that calls 'foo' with uninitialized variables, demonstrating a potential use case.

```c
void main()
{
size_t size;
char *arr;
arr_fun_t arr_fun;
foo(arr, size, arr_fun);
}
```

--------------------------------

### Get Functions Reachable Within N Steps (Single)

Source: https://diffblue.github.io/cbmc/call__graph__helpers_8h_source.html

Finds all functions reachable from a single start function within a specified number of steps.

```APIDOC
## get_functions_reachable_within_n_steps (Single)

### Description
Finds all functions reachable from a single start function within a specified number of steps in the call graph.

### Signature
std::set<irep_idt> get_functions_reachable_within_n_steps(const call_grapht::directed_grapht &graph, const irep_idt &start_function, std::size_t n);

### Parameters
- **graph** (const call_grapht::directed_grapht &) - The directed graph representation of the call graph.
- **start_function** (const irep_idt &) - The function from which to start the search.
- **n** (std::size_t) - The maximum number of steps to traverse.
```

--------------------------------

### Get Functions Reachable Within N Steps (Set)

Source: https://diffblue.github.io/cbmc/call__graph__helpers_8h_source.html

Finds all functions reachable from a set of start functions within a specified number of steps.

```APIDOC
## get_functions_reachable_within_n_steps (Set)

### Description
Finds all functions reachable from a set of start functions within a specified number of steps in the call graph.

### Signature
std::set<irep_idt> get_functions_reachable_within_n_steps(const call_grapht::directed_grapht &graph, const std::set<irep_idt> &start_functions, std::size_t n);

### Parameters
- **graph** (const call_grapht::directed_grapht &) - The directed graph representation of the call graph.
- **start_functions** (const std::set<irep_idt> &) - A set of functions from which to start the search.
- **n** (std::size_t) - The maximum number of steps to traverse.
```

--------------------------------

### smt2_parsert::setup_commands

Source: https://diffblue.github.io/cbmc/smt2__parser_8h_source.html

Sets up the internal map of command parsing functions.

```APIDOC
## smt2_parsert::setup_commands

### Description
Initializes the `commands` map, which associates string keys with functions that can execute SMT2 commands.

### Method
`void setup_commands()`

### Parameters
None

### Returns
None
```

--------------------------------

### Symex With State - symex_main.cpp

Source: https://diffblue.github.io/cbmc/goto__symex_8h_source.html

Symbolically executes the entire program starting from the entry point, given an initial state.

```cpp
virtual symbol_tablet symex_with_state(statet &state, const get_goto_functiont &get_goto_functions)
{
Symbolically execute the entire program starting from entry point.
}

```

--------------------------------

### Get SMT Solver Process Description

Source: https://diffblue.github.io/cbmc/smt__solver__process_8cpp_source.html

Returns a string describing the command line used to start the SMT solver process. This is useful for logging or debugging.

```cpp
const std::string &smt_piped_solver_processt::description()
{
 return command_line_description;
}
```

--------------------------------

### Example INVARIANT Macro Usage

Source: https://diffblue.github.io/cbmc/src_2util_2invariant_8h_source.html

Demonstrates the basic usage of the INVARIANT macro with a condition and a reason string. The reason should be a string literal starting with a lowercase character.

```cpp
INVARIANT(
 x > 0,
 "x should have a positive value as others are handled by other branches");
```

--------------------------------

### setup_expressions()

Source: https://diffblue.github.io/cbmc/classsmt2__solvert.html

Sets up the expressions for the SMT2 solver.

```APIDOC
## void setup_expressions()

### Description
Sets up the expressions for the SMT2 solver.

### Method
void protected
```

--------------------------------

### Get Destructors in Range

Source: https://diffblue.github.io/cbmc/scope__tree_8cpp_source.html

Retrieves a list of destructors within a specified range of the scope tree. It traverses from a starting index up to an ending index, collecting destructor information.

```cpp
const std::vector<destructor_and_idt> scope_treet::get_destructors(
std::optional<node_indext> end_index,
std::optional<node_indext> starting_index)
{
node_indext next_id = starting_index.value_or(get_current_node());
node_indext end_id = end_index.value_or(0);

std::vector<destructor_and_idt> codes;
while(next_id > end_id)
{
auto node = scope_graph[next_id];
auto &destructor = node.destructor_value;
if(destructor)
codes.emplace_back(destructor_and_idt(*destructor, next_id));

next_id = node.in.begin()->first;
}

return codes;
}
```

--------------------------------

### Display Help Mode

Source: https://diffblue.github.io/cbmc/ms__cl__mode_8cpp_source.html

Prints a message indicating that goto-cl understands CL options plus additional ones.

```cpp
void ms_cl_modet::help_mode()
{
std::cout << "goto-cl understands the options of CL plus the following.\n\n";
}
```

--------------------------------

### Compile and Generate Harness Example

Source: https://diffblue.github.io/cbmc/man/goto-harness.html

Demonstrates the typical sequence of compiling a C program, generating a harness for a specific function using goto-harness, and then running CBMC checks on the generated harness.

```bash
# Compile the program
goto-cc program.c -o program.gb
# Run goto-harness to produce harness file
goto-harness --harness-type call-function --harness-function-name generated_harness_test_function
  --function test_function program.gb harness.c
# Run the checks targeting the generated harness
cbmc --pointer-check harness.c --function generated_harness_test_function
```

--------------------------------

### Get Initial NFA State

Source: https://diffblue.github.io/cbmc/nfa_8h_source.html

Initializes and returns an NFA state set starting from a given initial state, including all reachable states via epsilon transitions.

```cpp
statet initial_state(state_labelt initial) const
{
statet result{};
result.possible_states.insert(initial);
follow_epsilon_transitions(result);
return result;
}
```

--------------------------------

### Initialize Symex State

Source: https://diffblue.github.io/cbmc/symex__main_8cpp_source.html

Initializes the state for symbolic execution, including shadow memory fields. This function is used as a setup step before starting the symbolic execution process.

```cpp
symex_with_state(*state, get_goto_function);
}
```

--------------------------------

### help()

Source: https://diffblue.github.io/cbmc/classgoto__instrument__parse__optionst.html

Displays command-line help information for the instrumentation tool.

```APIDOC
## help()

### Description
Displays command-line help information.
```

--------------------------------

### initialize [1/2]

Source: https://diffblue.github.io/cbmc/classflow__insensitive__analysis__baset.html

Initializes the analysis with goto functions. This is an inline virtual method.

```APIDOC
## initialize() [1/2]

### Description
Initializes the analysis with goto functions.

### Signature
`virtual void flow_insensitive_analysis_baset::initialize(const goto_functionst &)`

### Modifiers
inline virtual

### Reimplementation Notes
Reimplemented in `value_set_analysis_fit`.

### Definition
`flow_insensitive_analysis.h`, line 119
```

--------------------------------

### Get Restriction by Name

Source: https://diffblue.github.io/cbmc/restrict__function__pointers_8cpp_source.html

Retrieves a function pointer restriction by name for a given goto_function and location. This snippet is a precondition check and the start of a function that would likely look up restrictions.

```cpp
std::optional<function_pointer_restrictionst::restrictiont>
function_pointer_restrictionst::get_by_name_restriction(
 const goto_functiont &goto_function,
 const function_pointer_restrictionst::restrictionst &by_name_restrictions,
 const goto_programt::const_targett &location)
{
 PRECONDITION(location->is_function_call());

 const exprt &function = location->call_function();

```

--------------------------------

### Prehead Block Comment Example

Source: https://diffblue.github.io/cbmc/dfcc__instrument__loop_8cpp_source.html

A comment block illustrating the expected actions within the prehead instrumentation phase, including variable declarations, initializations, and setup for the write set.

```cpp
// ```
// ... preamble ...
//
// // Prehead block: Declare & initialize instrumentation variables
// // snapshot loop_entry history vars;
// // entered_loop = false
// // initial_invariant = loop_invariant;
// // in_base_case = true;
// // __ws_loop;
// // ws_loop := address_of(__ws_loop);
// // __write_set_create(ws_loop);
// // __write_set_add(ws_loop, loop_assigns);
// // __write_set_add(ws_loop, local_statics);
// // GOTO HEAD;
// // ```
```

--------------------------------

### initialize (whole program)

Source: https://diffblue.github.io/cbmc/classcustom__bitvector__analysist.html

Initializes all abstract states for a whole program.

```APIDOC
## initialize

### Description
Initialize all the abstract states for a whole program.

### Method
`void initialize(const goto_functionst &_goto_functions)`

### Parameters
- **_goto_functions** (const goto_functionst &) - The goto functions representing the whole program.
```

--------------------------------

### Get SMT2 Binary Numeral Token

Source: https://diffblue.github.io/cbmc/smt2__tokenizer_8cpp_source.html

Parses and returns a binary numeral token. It expects a sequence starting with '#b' followed by '0' or '1' characters. Handles end-of-file conditions.

```cpp
smt2_tokenizert::tokent smt2_tokenizert::get_bin_numeral()
{
 // we accept any sequence of '0' or '1'

 buffer.clear();
 buffer+='#';
 buffer+='b';

 char ch;
 while(in->get(ch))
 {
 if(ch=='0' || ch=='1')
 {
 buffer+=ch;
 }
 else
 {
 in->unget(); // put back
 return NUMERAL;
 }
 }

 // eof -- this is ok here
 if(buffer.empty())
 return END_OF_FILE;
 else
 return NUMERAL;
}
```

--------------------------------

### help()

Source: https://diffblue.github.io/cbmc/classsymtab2gb__parse__optionst.html

Displays help information for the symtab2gb tool.

```APIDOC
## void help()

### Description
Prints the help message for the symtab2gb tool to the console.

### Returns
void. Reimplemented from parse_options_baset::help.
```

--------------------------------

### Get Most Recent GDB Record

Source: https://diffblue.github.io/cbmc/gdb__api_8cpp_source.html

Reads the most recent line from GDB, checks if it starts with a given tag, and parses it as a GDB output record. Can optionally enforce that the record must exist.

```cpp
gdb_apit::gdb_output_recordt
gdb_apit::get_most_recent_record(const std::string &tag, const bool must_exist)
{
std::string line = read_most_recent_line();
const bool b = has_prefix(line, tag);

if(must_exist)
{
CHECK_RETURN(b);
}
else if(!b)
{
throw gdb_interaction_exceptiont("record does not exist");
}

std::string record = strip_string(line.substr(line.find(',') + 1));

return parse_gdb_output_record(record);
}
```

--------------------------------

### setup_symex

Source: https://diffblue.github.io/cbmc/classsingle__path__symex__only__checkert.html

Sets up the symbolic execution environment. This is an inline, protected, virtual method that can be reimplemented by derived classes.

```APIDOC
## setup_symex()

### Description
Sets up the symbolic execution environment.

### Parameters
- **symex** (symex_bmct&) - The symbolic execution object.

### Method
inline protected virtual

### Reimplemented in
java_single_path_symex_checkert, and java_single_path_symex_only_checkert

### Definition
Line 51 of file single_path_symex_only_checker.h.
```

--------------------------------

### java_entry_point()

Source: https://diffblue.github.io/cbmc/java__entry__point_8h.html

Generates a new function `__CPROVER__start` to call the method under test. It handles parameter initialization, method invocation, and output variable declaration. It also includes logic for non-deterministically setting input parameters to null or stack-allocated objects when `assume_init_pointers_not_null` is false, with considerations for array lengths and object tree depth.

```APIDOC
## java_entry_point()

### Description
Given the `symbol_table` and the `main_class` to test, this function generates a new function `__CPROVER__start` that calls the method under tests. If `__CPROVER__start` is already in the `symbol_table`, it silently returns. Otherwise it finds the method under test using `get_main_symbol` and constructs a body for `__CPROVER__start` which does as follows:
  1. Allocates and initializes the parameters of the method under test.
  2. Call it and save its return variable in the variable 'return'.
  3. Declare variable 'return' as an output variable using a `code_outputt`, together with other objects possibly altered by the execution of the method under test (in `java_record_outputs`).

When `assume_init_pointers_not_null` is false, the generated parameter initialization code will non-deterministically set input parameters to either null or a stack-allocated object. Observe that the null/non-null setting only applies to the parameter itself, and is not propagated to other pointers that it might be necessary to initialize in the object tree rooted at the parameter. Parameter `max_nondet_array_length` provides the maximum length for an array used as part of the input to the method under test, and `max_nondet_tree_depth` defines the maximum depth of the object tree created for such inputs. This maximum depth is used **in conjunction** with the so-called "recursive type set" (see field `recursive_set` in class java_object_factoryt) to bound the depth of the object tree for the parameter. Only when
  * the depth of the tree is >= max_nondet_tree_depth **AND**
  * the type of the object under initialization is already found in the recursive set then that object is not initalized and the reference pointing to it is (deterministically) set to null. This is a source of underapproximation in our approach to test generation, and should perhaps be fixed in the future.

### Parameters
- **symbol_table** (class symbol_table_baset &) - Global symbol table
- **main_class** (const irep_idt &) - Identifier of a class within which the main method to be analysed exists. This may be empty if the intention is not to analyse the main method.
- **message_handler** (class message_handlert &) - Where to write output to.
- **assume_init_pointers_not_null** (bool) - If this is true then any reference type parameters to the function under tests are assumed to be non-null.
- **assert_uncaught_exceptions** (bool) - Add an uncaught-exception check.
- **object_factory_parameters** (const java_object_factory_parameterst &) - Parameters for creation of arguments.
- **pointer_type_selector** (const select_pointer_typet &) - Logic for substituting types of pointers.
- **string_refinement_enabled** (bool) - If true, string refinement's string data structure will also be initialised and added to the symbol table.
- **build_arguments** (const build_argumentst &) - The function which builds the `codet`s which initialise the arguments for a function.

### Returns
- bool - true if error occurred on entry point search

### Definition
Line 602 of file java_entry_point.cpp.
```

--------------------------------

### Get Functions Reachable Within N Steps (Single Input)

Source: https://diffblue.github.io/cbmc/call__graph__helpers_8cpp_source.html

Finds all functions reachable from a single start function within a specified number of steps. This is a convenience overload for the set-based version.

```cpp
std::set<irep_idt> get_functions_reachable_within_n_steps(
    const call_grapht::directed_grapht &graph,
    const irep_idt &start_function,
    std::size_t n)
{
    std::set<irep_idt> start_functions({start_function});
    return get_functions_reachable_within_n_steps(graph, start_functions, n);
}
```

--------------------------------

### Setup Class Load Limit with Regex or Set

Source: https://diffblue.github.io/cbmc/java__class__loader__limit_8cpp_source.html

Initializes the class loader limit. Use a regex if the input string does not start with '@', otherwise parse a JSON configuration for a set of class files.

```cpp
void java_class_loader_limitt::setup_class_load_limit(
    const std::string &java_cp_include_files)
{
    PRECONDITION(!java_cp_include_files.empty());

    // '@' signals file reading with list of class files to load
    use_regex_match = java_cp_include_files[0] != '@';
    if(use_regex_match)
    {
        regex_matcher=std::regex(java_cp_include_files);
        log.debug() << "Limit loading to classes matching '" 
                    << java_cp_include_files << "'" << messaget::eom;
    }
    else
    {
        PRECONDITION(java_cp_include_files.length() > 1);
        jsont json_cp_config;
        if(parse_json(
            java_cp_include_files.substr(1),
            log.get_message_handler(),
            json_cp_config))
            throw "cannot read JSON input configuration for JAR loading";
        if(!json_cp_config.is_object())
            throw "the JSON file has a wrong format";
        jsont include_files=json_cp_config["classFiles"];
        if(!include_files.is_null() && !include_files.is_array())
            throw "the JSON file has a wrong format";
        for(const jsont &file_entry : to_json_array(include_files))
        {
            PRECONDITION(file_entry.is_string());
            set_matcher.insert(file_entry.value);
        }
    }
}
```

--------------------------------

### help()

Source: https://diffblue.github.io/cbmc/classgoto__diff__parse__optionst.html

Displays the command-line help information for the goto-diff tool.

```APIDOC
## help()

### Description
Displays command line help information.

### Returns
void
```

--------------------------------

### Main Execution Logic for Symtab2GB

Source: https://diffblue.github.io/cbmc/symtab2gb__parse__options_8cpp_source.html

Handles command-line arguments, sets up configuration, and initiates the conversion process. Throws exceptions for invalid arguments or file operations.

```cpp
int symtab2gb_parse_optionst::doit()
{
    if(cmdline.isset("version"))
    {
        log.status() << CBMC_VERSION << '\n';
        return CPROVER_EXIT_SUCCESS;
    }
    if(cmdline.args.empty())
    {
        throw invalid_command_line_argument_exceptiont{
            "expect at least one input file", "<json-symtab-file>"};
    }
    std::vector<std::string> symtab_filenames = cmdline.args;
    std::string gb_filename = "a.out";
    if(cmdline.isset(SYMTAB2GB_OUT_FILE_OPT))
    {
        gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT);
    }

    std::string goto_functions_filename_or_empty =
        cmdline.get_value(SYMTAB2GB_GOTO_FUNCTIONS_OPT);

    register_languages();
    config.set(cmdline);
    run_symtab2gb(
        symtab_filenames,
        gb_filename,
        goto_functions_filename_or_empty,
        cmdline.get_value("verbosity"));
    return CPROVER_EXIT_SUCCESS;
}
```