### Loop Assigns Inference Example Setup

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-assigns.md

Sets up helper functions and variables for demonstrating loop assigns inference.

```c
int j;

void set_j(int i)
{
  j = i;
}

void incr(int *n)
{
  (*n)++;
}
```

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

### Install goto-inspect Binary

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-inspect/CMakeLists.txt

Installs the built goto-inspect executable to the system's binary directory.

```cmake
install(TARGETS goto-inspect DESTINATION ${CMAKE_INSTALL_BINDIR})
```

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

### Install Man Page

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-inspect/CMakeLists.txt

Installs the man page for goto-harness if not on a Windows system.

```cmake
if(NOT WIN32)
  install(
    DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/
    DESTINATION ${CMAKE_INSTALL_MANDIR}/man1
    FILES_MATCHING PATTERN "goto-harness*"
  )
endif()
```

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

### Install npm package

Source: https://github.com/diffblue/cbmc/blob/develop/scripts/benchmark/README.md

Run this command to install the necessary npm package for the benchmarking scripts.

```bash
npm install
```

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

### Install goto-analyzer executable

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-analyzer/CMakeLists.txt

Installs the compiled goto-analyzer executable to the system's binary directory.

```cmake
install(TARGETS goto-analyzer DESTINATION ${CMAKE_INSTALL_BINDIR})
```

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

### LLVM-style Doxygen Documentation Example

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Provides an example of Doxygen documentation following LLVM guidelines, including detailed parameter and return value descriptions.

```cpp
/// This is the brief description (first sentence).
///
/// More detailed explanation can follow in subsequent paragraphs.
/// Feel free to break into multiple paragraphs for readability.
///
/// \param param1: Short description
/// \param param2: Longer description that needs multiple lines.
///   Additional lines indented by two spaces for clarity.
/// \param [out] output: This parameter is modified by the function
/// \return Description of return value
```

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

### Install Documentation Tools on Ubuntu

Source: https://github.com/diffblue/cbmc/blob/develop/doc/doxygen-root/README.md

Installs doxygen, graphviz, and pandoc using apt on Ubuntu. This command requires sudo privileges.

```bash
sudo apt install doxygen graphviz pandoc
```

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

### Install man page

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-analyzer/CMakeLists.txt

Installs the man page for goto-analyzer to the system's man directory, excluding Windows systems.

```cmake
if(NOT WIN32)
  install(
    DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/
    DESTINATION ${CMAKE_INSTALL_MANDIR}/man1
    FILES_MATCHING PATTERN "goto-analyzer*"
  )
endif()
```

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

### Install Documentation Tools on MacOS

Source: https://github.com/diffblue/cbmc/blob/develop/doc/doxygen-root/README.md

Installs doxygen, graphviz, and pandoc using Homebrew on macOS. Ensure Homebrew is installed before running this command.

```bash
brew install doxygen graphviz pandoc
```

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

### Unit Test Case Example

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

A basic example of a unit test written using the Catch2 testing framework, demonstrating a test case with setup, assertions, and tagging.

```cpp
TEST_CASE("My feature test", "[my-module]")
{
  // Setup
  // Test
  REQUIRE(result == expected);
}
```

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

### C Code Example: File1.c

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/README.md

Illustrates a simple C source file with a main function and a foo function.

```c
int main(){
  int x = 5;
  if(x > 7){
    x = 9; } } 

void foo(){}
```

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

### Setup JBMC Submodules

Source: https://github.com/diffblue/cbmc/blob/develop/jbmc/README.md

Set up the necessary submodules for the JBMC project before compilation.

```bash
make -C jbmc/src setup-submodules
```

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

### Install JDK and Maven on Debian/Ubuntu

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs Java Development Kit and Maven for JBMC compilation on Debian-based systems.

```bash
apt-get install openjdk-8-jdk maven jq
```

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

### Install Solaris Development Tools

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs GCC C++ compiler, Bison, and Flex on Solaris.

```bash
pkg install gcc-c++-7 bison flex
```

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

### Install FreeBSD Development Tools

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs essential build tools, version control, scripting languages, and SAT solvers on FreeBSD.

```bash
pkg install bash gmake git www/p5-libwww python python3 patch flex bison cvc5 z3
```

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

### Install FreeBSD JBMC Dependencies

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs JDK, wget, and Maven for JBMC compilation on FreeBSD.

```bash
pkg install openjdk8 wget maven
```

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

### Install clang-format on Ubuntu/Debian

Source: https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md

Installs the clang-format package using apt-get. This command is for Debian-based Linux distributions.

```shell
apt-get install clang-format
```

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

### Install macOS Development Tools

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs Xcode command-line tools for C/C++ compilation on macOS.

```bash
xcode-select --install
```

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

### Install JDK and Maven on Red Hat/Fedora

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs Java Development Kit and Maven for JBMC compilation on Red Hat-based systems.

```bash
dnf install java-1.8.0-openjdk-devel maven jq
```

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

### Install Debian/Ubuntu Dependencies

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs C/C++ compiler, build tools, and version control for Debian-based systems.

```bash
apt-get install g++ gcc flex bison make git curl patch
```

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

### test.desc Format Example

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Example of the content and format for a test.desc file, specifying test tags, input file, command-line options, and expected output.

```text
CORE
main.c
--bounds-check --unwind 5
^VERIFICATION SUCCESSFUL$
```

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

### C Code Example: File2.c

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/README.md

Illustrates a simple C source file with a bar function.

```c
char bar(){ }
```

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

### Install Pre-commit Hook

Source: https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md

Installs the pre-commit hook for cpplint. Run this command to copy the hook script to the .git/hooks directory.

```shell
cp .githooks/pre-commit .git/hooks/pre-commit
```

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

### Example: foo Function Implementation

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-assigns.md

A function 'foo' that calls the 'sum' function, demonstrating a typical usage scenario.

```c
int foo()
{
  uint32_t a;
  uint32_t b;
  uint32_t out;
  int rval = sum(a, b, &out);
  if (rval == SUCCESS)
    return out;
  return rval;
}
```

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

### Example Call Graph Output

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/README.md

This is an example of the output produced by the `goto-instrument --call-graph` command. The last lines indicate which functions call other functions.

```text
Reading GOTO program from `a.out'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
main -> fun
__CPROVER__start -> __CPROVER_initialize
__CPROVER__start -> main
fun -> malloc
```

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

### Function Doxygen Documentation Example

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Illustrates the Doxygen tags for documenting function parameters, return values, and providing a detailed description.

```cpp
/// Brief description ending with period. Longer description can follow.
/// \param arg: Description of parameter
/// \param [out] result: Output parameter description
/// \param [in,out] state: In-out parameter description
/// \return Description of return value
int my_function(int arg, int &result, state_t &state);
```

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

### Install Red Hat/Fedora Dependencies

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs C/C++ compiler, build tools, and version control for Red Hat-based systems.

```bash
dnf install gcc gcc-c++ flex bison curl patch
```

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

### C Program Example

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/properties.md

A simple C program with a potential NULL-pointer dereference, used as an example for goto-instrument.

```c
int *ptr;

int main(void) {
  if (ptr)
    *ptr = 0;
  if (!ptr)
    *ptr = 1;
}
```

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

### Install Man Page

Source: https://github.com/diffblue/cbmc/blob/develop/src/memory-analyzer/CMakeLists.txt

Installs the man page for the memory-analyzer on non-Windows systems. It specifies the source directory and the destination for the man files.

```cmake
if(NOT WIN32)
  install(
    DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/
    DESTINATION ${CMAKE_INSTALL_MANDIR}/man1
    FILES_MATCHING PATTERN "memory-analyzer*"
  )
endif()
```

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

### C Code Example

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/README.md

This is the original C code that will be translated into a goto-program.

```c
unsigned mult(unsigned a, unsigned b)
{
  int acc = 0, i;
  for (i = 0; i < b; i++)
    acc += a;
  return acc;
}
```

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

### Bash Autocomplete Example

Source: https://github.com/diffblue/cbmc/blob/develop/scripts/bash-autocomplete/README.md

Demonstrates how to use bash autocomplete by typing a partial switch and pressing TAB.

```bash
cbmc --clas<TAB>
```

```bash
cbmc --classpath
```

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

### String Solver Example

Source: https://github.com/diffblue/cbmc/blob/develop/src/solvers/README.md

This example demonstrates how to use the string solver for string manipulation and comparison. It involves concatenating strings and checking for equality.

```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
```

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

### Java Code Example with StringBuilder

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/jbmc-user-manual.md

Example Java code demonstrating StringBuilder operations, used to test Java Library support in JBMC.

```java
package tutorial;

public class ExampleModels {

    public static void main(String[] args) {
        StringBuilder sb = new StringBuilder("abcd");
        StringBuilder sb2 = sb.insert(2, "$");
        assert sb2.toString().startsWith("abc");
    }

}
```

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

### Custom MMIO Read Implementation Example

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/modeling-mmio.md

Provide a custom implementation for `__CPROVER_mm_io_r` to define specific behavior for reads at certain addresses. This example returns a fixed value for address 0x1000 and non-deterministic values otherwise.

```c
char __CPROVER_mm_io_r(void *a, unsigned s) {
  if(a == 0x1000)
    return 2;
  else
    return nondet_char();
}
```

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

### Install Build Dependencies on Debian-like Systems

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs essential build tools including C++ compiler, flex, bison, make, git, curl, patch, and CMake.

```bash
apt-get install g++ gcc flex bison make git curl patch cmake
```

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

### Pointer Arithmetic Example

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/modeling-pointers.md

Demonstrates how pointer arithmetic translates to object offsets. Note that pointer arithmetic is byte-granular.

```C
unsigned array[10];
char *p;

p=(char *)(array+1);
p++;
```

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

### Java Get Current Thread ID

Source: https://github.com/diffblue/cbmc/blob/develop/jbmc/src/java_bytecode/README.md

Example of Java code to retrieve the current thread's ID. This is converted to access a thread-local variable in the intermediate representation.

```java
  int g = java.lang.thead.getCurrentThreadId();
```

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

### C Code Example for Memory Snapshot

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/goto-harness.md

This C code includes functions for getting random values and clipping integers, with an assertion to be verified. The snapshot is intended to be taken after specific function calls.

```C
// main.c
#include <assert.h>
#include <stdlib.h>

int x;
int y;
int z;

// complex function which returns 1
int get_one()
{
  int i;

  for(i = 0; i < 100001; i++)
  {
    if(rand() && ((i & 1) == 1))
      break;
  }

  return i & 1;
}

// return a random value (!= 0)
int get_random_value()
{
  int r;
  while((r = rand()) == 0) {}
  return r;
}

int clip(int i)
{
  if(i > 99)
  {
    i = 99;
  }

  return i;
}

int main()
{
  x = get_random_value();
  y = get_one();

  // snapshot taken here (line 46)

  z = clip(x);

  assert(y + z <= 100);

  return 0;
}

```

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

### Display JBMC Help

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/jbmc-user-manual.md

Run `jbmc --help` to display a list of all available options for JBMC.

```bash
$ jbmc --help
```

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

### Specify Assignable Memory with __CPROVER_object_from

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-assigns.md

Use __CPROVER_object_from to specify that the range of bytes starting at 'ptr' up to the end of the object is assignable. This allows assignments to the hidden byte but still rejects assignments to 'vec->size' in the example.

```c
void __CPROVER_object_from(void *ptr);
```

```c
#include <stdlib.h>

#define MAX_SIZE 10

struct vec_t {
  size_t size;
  char *data;
};

// Allocates a vect_t struct together with its data and a hidden byte
// in a same object.
struct vec_t *vec_alloc(size_t size) {

  if(size > MAX_SIZE)
    size = MAX_SIZE;

  // allocate the struct + data + 1 extra hidden byte
  struct vec_t *vec = malloc(sizeof(struct vec_t) + size + 1);
  if (vec) {
    vec->size = size;
    vec->data = ((char *)vec) + sizeof(struct vec_t);
  }
  return vec;
}

// Clear the vec->data array
void vec_clear(struct vec_t *vec)
  __CPROVER_assigns(
    vec && vec->data: __CPROVER_object_from(vec->data))
{
  if (!vec)
    return;

  vec->size = vec->size; // FAILURE

  for (size_t i = 0; i < vec->size; i++)
    vec->data[i] = 0; // SUCCESS

  char *hidden_byte = ((char *)vec + sizeof(*vec) + vec->size);
  *hidden_byte = 0; // SUCCESS
}

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

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

### Specify Assignable Memory with __CPROVER_object_upto

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-assigns.md

Use __CPROVER_object_upto to specify that a range of bytes starting at 'ptr' with a given 'size' is assignable. The size must not exceed the object's boundary. This example shows how assignments to 'vec->size' and a hidden byte fail verification when only the data array is marked as assignable.

```c
void __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
```

```c
#include <stdlib.h>

#define MAX_SIZE 10

struct vec_t {
  size_t size;
  char *data;
};

// Allocates a vect_t struct together with its data and a hidden byte
// in a same object.
struct vec_t *vec_alloc(size_t size) {

  if(size > MAX_SIZE)
    size = MAX_SIZE;

  // allocate the struct + data + 1 extra hidden byte
  struct vec_t *vec = malloc(sizeof(struct vec_t) + size + 1);
  if (vec) {
    vec->size = size;
    vec->data = ((char *)vec) + sizeof(struct vec_t);
  }
  return vec;
}

// Clear the vec->data array
void vec_clear(struct vec_t *vec)
  __CPROVER_assigns(
    vec && vec->data: __CPROVER_object_upto(vec->data, vec->size))
{
  if (!vec)
    return;

  vec->size = vec->size; // FAILURE

  for (size_t i = 0; i < vec->size; i++)
    vec->data[i] = 0; // SUCCESS

  char *hidden_byte = ((char *)vec + sizeof(*vec) + vec->size);
  *hidden_byte = 0; // FAILURE
}

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

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

### Install CBMC using Homebrew

Source: https://github.com/diffblue/cbmc/blob/develop/README.md

Use this command to install the latest version of CBMC if you have Homebrew installed.

```sh
$ brew install cbmc
```

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

### Install clang-format on macOS

Source: https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md

Installs the clang-format package using Homebrew. This command is for macOS users with Homebrew installed.

```shell
brew install clang-format
```

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

### Get Help for goto-diff

Source: https://github.com/diffblue/cbmc/blob/develop/TOOLS_OVERVIEW.md

Run this command to view all available options for the goto-diff tool, including those for difference checking and goto program instrumentation.

```bash
goto-diff --help
```

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

### Working with GOTO Programs

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Commands for generating, viewing, instrumenting, and verifying GOTO programs using goto-cc, goto-instrument, and CBMC.

```bash
# Generate GOTO binary from C code
goto-cc -o program.gb program.c
# View GOTO program
goto-instrument --show-goto-functions program.gb

# Instrument GOTO program
goto-instrument --bounds-check program.gb instrumented.gb

# Verify with CBMC
cbmc instrumented.gb
```

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

### Run unit tests with Make

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Execute unit tests by navigating to the 'unit' directory and running 'make test'.

```bash
cd unit
make test
```

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

### Build goto-binaries with MSBuild

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/visual-studio.md

Use this command in the Visual Studio Command Prompt to build goto-binaries from your Visual Studio project. Ensure goto-cl.exe and goto-link.exe are in your PATH and the 'Flavor' matches your configuration manager setting.

```bash
msbuild /p:CLToolExe=goto-cl.exe /p:LinkToolExe=goto-link.exe    /p:Flavor=goto-cc /p:Platform=x86
```

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

### Install Build Dependencies on macOS

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs Xcode command-line tools and CMake via Homebrew.

```bash
xcode-select --install
```

```bash
brew install cmake
```

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

### JBMC Command to Analyze ExampleArray

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/jbmc-user-manual.md

Run this command to have JBMC analyze the ExampleArray.java for potential runtime errors.

```bash
$ jbmc tutorial.ExampleArray
```

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

### Remove CBMC Version

Source: https://github.com/diffblue/cbmc/blob/develop/doc/ADR/homebrew_tap.md

Remove a previously installed version of CBMC that was installed using the tap.

```bash
$ brew remove diffblue/cbmc/cbmc@5.54.0
```

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

### Using Z3 Solver with Incremental SMT Backend

Source: https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2_incremental/README.md

Example of how to invoke the Z3 solver using the incremental SMT backend. Ensure Z3 is in your PATH or provide the full executable path.

```bash
--incremental-smt2-solver 'z3 -smt2 -in'
```

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

### Create a General Reference Link

Source: https://github.com/diffblue/cbmc/blob/develop/doc/doxygen-root/contributing.md

Use the \ref command to create a link to a documentation page from any other file. You can specify custom link text to improve readability and context.

```doxygen
\ref child "link text"
```

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

### Generate and view goto-program as a PNG diagram

Source: https://github.com/diffblue/cbmc/blob/develop/doc/architectural/howto.md

Generate a graphical representation of a goto-program using goto-instrument and the dot command. The output is saved as a PNG file and opened in the default image viewer.

```bash
goto-instrument --dot main.gb | tail -n +2 | dot -Tpng > main.png
open main.png
```

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

### Java Code Example for Exception Handling

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/jbmc-user-manual.md

Example Java code with a method that may throw a NullPointerException.

```java
package tutorial;

public class ExampleExceptions {

    public static int strLength(String str) {
        return str.length();
    }

}
```

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

### Run Unit Tests

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Navigate to the unit test directory and execute the unit test binary. This command assumes the unit tests are located in a subdirectory named 'unit'.

```bash
cd unit && ../build/bin/unit
```

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

### Install Amazon Linux Dependencies

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs C/C++ compiler, build tools, and archiving utilities for Amazon Linux.

```bash
yum install gcc-c++ flex bison patch tar
```

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

### Using CVC5 Solver with Incremental SMT Backend

Source: https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2_incremental/README.md

Example of how to invoke the CVC5 solver using the incremental SMT backend. Ensure CVC5 is in your PATH or provide the full executable path.

```bash
--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental'
```

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

### JBMC Command to Analyze ExampleArraySafe

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/jbmc-user-manual.md

Run this command to analyze the corrected ExampleArraySafe.java with JBMC.

```bash
$ jbmc tutorial.ExampleArraySafe
```

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

### Generate Documentation

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Generate project documentation using Doxygen. This command should be run from the 'src' directory.

```bash
cd src && doxygen
```

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

### goto-harness Command for C String Initialization

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/goto-harness.md

This command generates a harness for the `function` that treats the `pointer` parameter as a C string. It uses `--treat-pointer-as-cstring` and `--associated-array-size` to ensure the pointer is initialized as a null-terminated string of the correct size.

```sh
$ goto-cc -o nondet_string.gb nondet_string.c
$ goto-harness \
  --harness-function-name harness \
  --harness-type call-function \
  --function function \
  --treat-pointer-as-cstring pointer \
  --associated-array-size pointer:size \
  nondet_string.gb nondet_string_harness.c
$ cbmc --function harness nondet_string_harness.c nondet_string.c --unwind 10
```

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

### Install Build Dependencies on Red Hat/Fedora

Source: https://github.com/diffblue/cbmc/blob/develop/COMPILING.md

Installs necessary build tools such as GCC, flex, bison, curl, patch, and CMake.

```bash
dnf install gcc gcc-c++ flex bison curl patch cmake
```

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

### Example XML Function Call Element

Source: https://github.com/diffblue/cbmc/blob/develop/doc/assets/xml_spec.md

An example of a 'function_call' element, showing a call to the 'main' function with its associated location information.

```xml
<function_call hidden="false" step_nr="20" thread="0">
  <function display_name="main" identifier="main">
    <location .. />
  </function>
  <location .. />
</function_call>
```

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

### goto-harness Command for Array Parameter Initialization

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/goto-harness.md

This command generates a harness for the `is_prefix_of` function, specifying that `string` is an array of size `string_length` and `prefix` is an array of size `prefix_length`. This helps in correctly initializing and verifying array parameters.

```sh
$ goto-cc -o array_example.gb array_example.c
$ goto-harness \
  --harness-function-name harness \
  --harness-type call-function \
  --function is_prefix_of \
  --associated-array-size string:string_length \
  --associated-array-size prefix:prefix_length \
  array_example.gb array_example_harness.c
$ cbmc --function harness --unwind 10 --pointer-check array_example_harness.c array_example.c
```

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

### Example XML Input Element

Source: https://github.com/diffblue/cbmc/blob/develop/doc/assets/xml_spec.md

An example of an 'input' element showing how a variable 'i' is initialized with a specific integer value and its internal representation.

```xml
<input hidden="false" step_nr="21" thread="0">
  <input_id>i</input_id>
  <value>-2147145201</value>
  <value_expression>
    <integer binary="10000000000001010010101000001111"
             c_type="int" width="32">
      -2147145201
    </integer>
  </value_expression>
  <location .. />
</input>
```

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

### Automated Harness Generation with `goto-harness`

Source: https://context7.com/diffblue/cbmc/llms.txt

Guide to using `goto-harness` for generating test harnesses that nondeterministically initialize function arguments and global state.

```APIDOC
## Automated Harness Generation with `goto-harness`

`goto-harness` generates test harnesses that nondeterministically initialize function arguments and global state, enabling isolated analysis of individual functions without writing harnesses by hand.

```sh
# Basic function-call harness
goto-cc main.c -o main.gb
goto-harness \
  --harness-function-name harness \
  --harness-type call-function \
  --function function_to_test \
  main.gb harness.c
cbmc --function harness harness.c main.c

# Harness for a function with linked list parameters
# (generates lists up to depth 4, minimum length 1, havocing globals)
goto-cc list_example.c -o list_example.gb
goto-harness \
  --harness-function-name harness \
  --harness-type call-function \
  --function check_list \
  --max-nondet-tree-depth 4 \
  --min-null-tree-depth 1 \
  --nondet-globals \
  list_example.gb list_example_harness.c
cbmc list_example.c list_example_harness.c \
  --function harness --unwind 20 --unwinding-assertions
# [check_list.assertion.2] line 55 assertion global_cursor->value == ...: FAILURE

# Harness for array parameters with associated size
goto-cc array_example.c -o array_example.gb
goto-harness \
  --harness-function-name harness \
  --harness-type call-function \
  --function is_prefix_of \
  --associated-array-size string:string_length \
  --associated-array-size prefix:prefix_length \
  array_example.gb array_example_harness.c
cbmc --function harness --unwind 10 --pointer-check \
  array_example_harness.c array_example.c
```
```

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

### Create GOTO Binary

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Compile a C source file into a GOTO binary format using goto-cc. The output is directed to 'out.gb'.

```bash
goto-cc -o out.gb input.c
```

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

### CMake Build Quick Start

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Commands to initialize, generate build files, and build the CBMC project using CMake. Ensure submodules are updated before generating build files.

```bash
# 1. Update submodules
git submodule update --init

# 2. Generate build files
cmake -S . -Bbuild

# 3. Build
cmake --build build --parallel $(nproc)

# 4. Run tests
ctest --test-dir build -V -L CORE
```

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

### Loop Invariant Example with __CPROVER_loop_entry

Source: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-history-variables.md

This example shows a loop invariant that asserts 'x <= 200' before and after each iteration by comparing 'x' with its value captured at loop entry.

```c
void my_function()
{
  unsigned x = 200;
  while( x >= 64 )
  __CPROVER_loop_invariant(x <= __CPROVER_loop_entry(x)) //equivalent to x <= 200
  {
    ...
    x -= 64;
  }
}
```

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

### XML Example for Source Location

Source: https://github.com/diffblue/cbmc/blob/develop/doc/assets/xml_spec.md

An example of how source location data is represented in CBMC trace XML, specifying file, function, line, and working directory.

```xml
<location file="test.c" function="main" line="7"
          working-directory="/tmp/subfolder"/>
```

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

### Benchmark Java Project with JBMC

Source: https://github.com/diffblue/cbmc/blob/develop/scripts/benchmark/README.md

Execute the main benchmarking script. Specify the path to JBMC, a method list file, JBMC arguments, and Java models library. Results are displayed and saved to a JSON file.

```bash
/path/to/scripts/benchmark/benchmark_java_project.js /path/to/jbmc -l method_list_example.txt -a jbmc_arguments_example.json -m path/to/jbmc/lib/java-models-library/target/core-models.jar | tee result.json
```

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

### Configure Java Alternatives

Source: https://github.com/diffblue/cbmc/blob/develop/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/README.md

Use this command to select the desired Java compiler version on your system. Ensure the compiler of interest is installed before configuring.

```bash
sudo update-alternatives --config javac
```

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

### Install CBMC Version via Tap

Source: https://github.com/diffblue/cbmc/blob/develop/doc/ADR/homebrew_tap.md

Install a specific version of CBMC by referencing its versioned formula from the added tap. The version must be built from source locally.

```bash
$ brew install diffblue/cbmc/cbmc@5.54.0
```

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

### Verify Linked List Example with CBMC

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/goto-harness.md

Command to verify the linked list example using CBMC after generating the harness. It includes unwinding assertions to handle loops in the code.

```sh
$ cbmc list_example.c list_example_harness.c --function harness --unwind 20 --unwinding-assertions
```

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

### Example Library and Harness for Public API

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/static-functions.md

Defines a public API function and a harness to check its contract. The harness uses __CPROVER_assume to set preconditions and __CPROVER_assert to check postconditions.

```C
void public_api_function(const int *a, int *b)
{
  // ...
  private_function(a, b);
  // ...
}

static void private_function(const int *a, int *b)
{
  // ...
}
```

```C
void public_api_function(int *a, int *b);

void harness()
{
  int a, b;
  __CPROVER_assume(a < 10);
  __CPROVER_assume(a >= 0);
  public_api_function(&a, &b);
  __CPROVER_assert(b != a);
}
```

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

### XML Example for Assertion Failure

Source: https://github.com/diffblue/cbmc/blob/develop/doc/assets/xml_spec.md

An example of an assertion failure element in CBMC trace XML, showing attributes like hidden, step number, thread, property, and reason.

```xml
<failure hidden="false" step_nr="23" thread="0"
         property="main.assertion.1"
         reason="assertion a + b &lt; 10">
  <location .. />
</failure>
```

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

### Java Example for Member Assignment

Source: https://github.com/diffblue/cbmc/blob/develop/jbmc/src/java_bytecode/README.md

Illustrates the assignment of values to fields of reference types, including nested objects. This example is used to detail the steps involved in complex object assignments.

```java
public class Example {
  static ReferenceTypeReferenceField globalReferenceTypeReferenceField;
  public static void assignReferenceTypes() {
    globalReferenceTypeReferenceField =
        new ReferenceTypeReferenceField(new ReferenceTypePrimitiveField(5));
}

class ReferenceTypeReferenceField {
  ReferenceTypePrimitiveField referenceField;
  public ReferenceTypeReferenceField(ReferenceTypePrimitiveField r) {
    referenceField = r;
  }
}

class ReferenceTypePrimitiveField {
  int primitiveField;
  public ReferenceTypePrimitiveField(int i) {
    primitiveField = i;
  }
}
```

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

### Example C Program for Error Detection

Source: https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/properties.md

A C program demonstrating potential error conditions that can be detected using CBMC's function body generation features. This example includes calls to `internal_error` and `api_error`.

```C
// error_example.c
#include <stdlib.h>

void api_error(void);
void internal_error(void);

int main(void)
{
  int arr[10] = {1,2,3,4,5, 6, 7, 8, 9, 10};
  int sum = 0;
  for(int i = 1; i < 10; ++i)
  {
    sum += arr[i];
  }
  if(sum != 55)
  {
    // we made a mistake when calculating the sum
    internal_error();
  }
  if(rand() < 0)
  {
    // we think this cannot happen
    api_error();
  }
  return 0;
}
```

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

### Run CPROVER on coreJSON

Source: https://github.com/diffblue/cbmc/blob/develop/src/cprover/README.md

Follow these steps to set up and run the CPROVER encoding and solver on the coreJSON library. Ensure the `cprover` binary is in your PATH before starting.

```sh
git clone https://github.com/kroening/coreJSON
cd coreJSON
git checkout cprover
cd test/cprover
./setup
./script
```

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

### Building CBMC Documentation with Doxygen

Source: https://github.com/diffblue/cbmc/blob/develop/AGENTS.md

Command to navigate to the source directory and run Doxygen to build the API documentation.

```bash
cd src
doxygen
# Output in doc/html/
```