C/C++ CTest Test Case Generation

Overview

ESBMC supports the automatic generation of CTest test cases for C and C++ programs from --branch-coverage or --k-path-coverage runs. Each reached coverage witness is materialised as a runnable CTest case with a concrete __VERIFIER_nondet_* implementation derived from the SMT model.

Dependencies

CMake (includes CTest)
GCC or Clang (with --coverage support)
gcovr
macOS only: Xcode Command Line Tools (provides xcrun llvm-cov gcov)

Usage

Basic Command

Generate multiple test cases (branch coverage mode):

esbmc program.c --branch-coverage --generate-ctest-testcase
esbmc program.cpp --branch-coverage --generate-ctest-testcase

Generate multiple test cases (k-path coverage mode):

esbmc program.c   --k-path-coverage --generate-ctest-testcase
esbmc program.cpp --k-path-coverage=2 --unwind 4 --no-unwinding-assertions --generate-ctest-testcase

The two modes differ in what each generated test exercises: --branch-coverage produces one test per reached branch direction, while --k-path-coverage[=N] produces one test per reached bounded path of length up to N conditional branches (PathCrawler-style). For programs with correlated branches or loops, k-path coverage typically yields more tests, each pinning down a longer prefix of branch outcomes. See the Coverage Analysis page for the full description of --k-path-coverage and its supporting flags (--k-path-witness-depth, --k-path-max-goals).

Both modes generate:

test_case_1.c / test_case_1.cpp, test_case_2.c / test_case_2.cpp, … - Test case implementations
CMakeLists.txt - CMake build configuration
esbmc_verifier.h - Forward declarations for __VERIFIER_* functions (force-included automatically)

The output file extension (.c or .cpp) and CMake language (C or CXX) are determined automatically from the input file extension. Files with .cpp, .cc, or .cxx extensions are treated as C++.

When two reached witnesses resolve to the same nondet input vector, the second is dropped — ESBMC prints Skipped N duplicate test case(s). so the generated test count may be smaller than the reached-witness count reported in [Coverage]. This is most visible under --k-path-coverage, where multiple bounded-path goals can share a single witness model.

Input Format

Your code should use functions like extern "C" int __VERIFIER_nondet_int(void); to mark symbolic inputs.

Declarations are optional. ESBMC provides these functions internally during verification, so you do not need to declare them yourself. For both C and C++, ESBMC automatically generates esbmc_verifier.h and force-includes it when building the generated tests, so the build works even if your source file has no declarations at all. If your source file does already declare them, duplicate declarations are harmless.

C (example.c):

#include <stdio.h>

/* Optional: Forward declarations are injected automatically at build time.
   You may also add by yourself */
extern int __VERIFIER_nondet_int(void);

static int compute(int a, int b) {
  if (a > 0) {
    if (b == 0) {
      return 10;
    } else {
      return 11;
    }
  } else {
    if (b < 0) {
      return 20;
    } else {
      return 21;
    }
  }
}

int main(void) {
  int a = __VERIFIER_nondet_int();
  int b = __VERIFIER_nondet_int();
  int r = compute(a, b);
  printf("%d\n", r);
  return 0;
}

C++ (example.cpp):

/* extern "C" int __VERIFIER_nondet_int(void); declaration is optional — ESBMC injects esbmc_verifier.h */

static int compute(int a, int b) {
  if (a > 0) {
    if (b == 0) {
      return 10;
    } else {
      return 11;
    }
  } else {
    if (b < 0) {
      return 20;
    } else {
      return 21;
    }
  }
}

int main() {
  int a = __VERIFIER_nondet_int();
  int b = __VERIFIER_nondet_int();
  int r = compute(a, b);
  return 0;
}

Output Format

Each generated test file provides concrete implementations of __VERIFIER_nondet_* and must not define main().

For both C and C++ projects, ESBMC also generates esbmc_verifier.h containing forward declarations for every __VERIFIER_* function. The generated CMakeLists.txt force-includes this header (via target_compile_options ... -include) when compiling the original source file, so the build succeeds regardless of whether the source declares these functions itself. The header uses #ifdef __cplusplus guards so the same file works for both languages.

C output (test_case_1.c):

// Auto-generated by ESBMC 7.11.0
// Test case 1 of 6
// This file provides concrete implementations of __VERIFIER_nondet_* functions

int __VERIFIER_nondet_int(void) {
  static int i = 0;
  static const int v[] = { -2147483633, 0 };
  return v[i++];
}

C++ output (test_case_1.cpp):

// Auto-generated by ESBMC 7.11.0
// Test case 1 of 6
// This file provides concrete implementations of __VERIFIER_nondet_* functions

extern "C" {

int __VERIFIER_nondet_int(void) {
  static int i = 0;
  static const int v[] = { -2147483633, 0 };
  return v[i++];
}

} // extern "C"

CMakeLists.txt (C):

# Auto-generated by ESBMC 7.11.0
cmake_minimum_required(VERSION 3.10)
project(ESBMCGeneratedTests C)

enable_testing()

option(ENABLE_COVERAGE "Enable coverage reporting" OFF)
if(ENABLE_COVERAGE AND CMAKE_C_COMPILER_ID MATCHES "GNU|Clang")
  add_compile_options(-O0 -g --coverage)
  add_link_options(--coverage)
endif()

# Each test case is compiled with the original source + test case implementation
add_executable(test_case_1 example.c test_case_1.c)
add_test(NAME test_case_1 COMMAND test_case_1)
# Force-include esbmc_verifier.h so the C source gets __VERIFIER_* declarations
# even if it does not declare them itself (required under strict C99+).
target_compile_options(test_case_1 PRIVATE -include ${CMAKE_CURRENT_SOURCE_DIR}/esbmc_verifier.h)
...

CMakeLists.txt (C++):

# Auto-generated by ESBMC 7.11.0
cmake_minimum_required(VERSION 3.10)
project(ESBMCGeneratedTests CXX)

enable_testing()

option(ENABLE_COVERAGE "Enable coverage reporting" OFF)
if(ENABLE_COVERAGE AND CMAKE_CXX_COMPILER_ID MATCHES "GNU|Clang")
  add_compile_options(-O0 -g --coverage)
  add_link_options(--coverage)
endif()

# Each test case is compiled with the original source + test case implementation
add_executable(test_case_1 example.cpp test_case_1.cpp)
add_test(NAME test_case_1 COMMAND test_case_1)
# Force-include esbmc_verifier.h so the C++ source gets extern "C" declarations
# even if it does not declare __VERIFIER_* functions itself.
target_compile_options(test_case_1 PRIVATE -include ${CMAKE_CURRENT_SOURCE_DIR}/esbmc_verifier.h)
...

esbmc_verifier.h (also generated):

// Auto-generated by ESBMC 7.11.0
// Forward declarations for __VERIFIER_* functions used in the verified source.
// This header is force-included by CMake so the source file compiles correctly
// even without explicit extern "C" declarations.
#pragma once
#ifdef __cplusplus
extern "C" {
#endif

int __VERIFIER_nondet_int(void);
void __VERIFIER_assume(int cond);
// ... one entry per __VERIFIER_* type used in the program

#ifdef __cplusplus
}
#endif

K-Path Worked Example

The k-path coverage mode is most informative on programs with correlated branches or loop bodies, where individual branch coverage misses interesting input combinations. The following loop-body example mirrors regression/goto-coverage/k_path_cov_2/:

loop.c:

extern int __VERIFIER_nondet_int(void);

int main(void)
{
  int x = __VERIFIER_nondet_int();
  for (int i = 0; i < 3; i++)
  {
    if (x > 0)
      x = x - 1;
    else
      x = x + 1;
  }
  return x;
}

Run ESBMC with --k-path-coverage=2 (prefix length 2) and --unwind 4 so the loop is fully unrolled:

esbmc loop.c --k-path-coverage=2 --unwind 4 --no-unwinding-assertions --generate-ctest-testcase

Expected coverage report and test-case generation summary:

[Coverage]

k-Path Witnesses : 6
Reached : 4
k-Path Coverage: 66.66666666666667%
Skipped 7 duplicate test case(s).
Generated 3 CTest test case(s) with CMakeLists.txt

Of the six bounded-path goals, four are reachable; the remaining two are infeasible because x > 0 does not flip across iterations without an external write. The multi-property witness loop calls into the test-case collector once per SAT verdict, accumulating ten raw witness models across the four reached goals (each goal can produce more than one model under multi-property enumeration). The dedup pass keys on the concrete __VERIFIER_nondet_int vector and keeps the three distinct ones — reported as Skipped 7 duplicate test case(s). — producing test_case_1.c, test_case_2.c, and test_case_3.c.

Tuning knobs. The supporting flags --k-path-witness-depth=D (post-simplification depth cap on witness guards, default 8) and --k-path-max-goals=M (per-function goal cap, default 10000) are propagated through to test-case generation unchanged: a witness that gets dropped under --k-path-witness-depth also produces no CTest case, and a goal-cap overflow aborts the run before any test cases are written. See Coverage Analysis for details.

Phase-1 limitation. The k-path instrumentation walks the goto program linearly to collect prior branch guards, which over-approximates the prefix when branches join: some witnesses reported as unreached are simply infeasible rather than indicative of missing test inputs. The number of generated test cases is therefore a lower bound on the reachable bounded paths. Tracked in issue #4325.

Compiling and Running Tests

Step 1: Build tests with coverage enabled

mkdir build && cd build
cmake -DENABLE_COVERAGE=ON ..
cmake --build .

Step 2: Run tests .gcda files are generated on program exit; you must run the tests (ctest) before running gcovr.

ctest -V

(Optional) Reset coverage counters before running:

find build -name "*.gcda" -delete

Step 3: Run with coverage

Generate coverage report using gcovr:

Linux:

gcovr -r .. --txt-metric branch --object-directory .

macOS (Xcode toolchain):

gcovr -r .. --txt-metric branch --object-directory . --gcov-executable "xcrun llvm-cov gcov"

Note: install gcovr if not present:

# Debian/Ubuntu
sudo apt install gcovr
# macOS
brew install gcovr

Example Results

Total Test time (real) =   0.01 sec
------------------------------------------------------------------------------
                           GCC Code Coverage Report
Directory: ..
------------------------------------------------------------------------------
File                                    Branches   Taken  Cover   Missing
------------------------------------------------------------------------------
example.c                                      6       6   100%
test_case_1.c                                  0       0    --%
...
------------------------------------------------------------------------------
TOTAL                                          6       6   100%
------------------------------------------------------------------------------

Supported Types

The CTest generator can format all types supported by ESBMC’s symbolic execution engine. These types are collected using the same logic as --generate-testcase (TestComp XML format) and then formatted as C or C++ code.

Integer Types (Signed)

Function	C Type	Example Values
`__VERIFIER_nondet_char()`	`char`	`-128, 0, 127`
`__VERIFIER_nondet_schar()`	`signed char`	`-128, 0, 127`
`__VERIFIER_nondet_short()`	`short`	`-32768, 0, 32767`
`__VERIFIER_nondet_int()`	`int`	`-2147483648, 0, 2147483647`
`__VERIFIER_nondet_long()`	`long`	`-2^63, 0, 2^63-1`

Integer Types (Unsigned)

Function	C Type	Example Values
`__VERIFIER_nondet_uchar()`	`unsigned char`	`0, 255`
`__VERIFIER_nondet_ushort()`	`unsigned short`	`0, 65535`
`__VERIFIER_nondet_uint()`	`unsigned int`	`0, 4294967295`
`__VERIFIER_nondet_ulong()`	`unsigned long`	`0, 2^64-1`

Floating-Point Types

Function	C Type	Example Values
`__VERIFIER_nondet_float()`	`float`	`0.0, 3.14, -1.5`
`__VERIFIER_nondet_double()`	`double`	`0.0, 2.718281828`

Boolean Type

Function	C Type	C++ Type	Example Values
`__VERIFIER_nondet_bool()`	`_Bool`	`bool`	`0, 1`

Example: Multiple Types

C (mixed_types.c):

#include <stdio.h>

/* Optional — esbmc_verifier.h is injected automatically at build time.*/
extern char __VERIFIER_nondet_char(void);
extern unsigned char __VERIFIER_nondet_uchar(void);
extern _Bool __VERIFIER_nondet_bool(void);

int main(void) {
  char c = __VERIFIER_nondet_char();
  unsigned char uc = __VERIFIER_nondet_uchar();
  _Bool b = __VERIFIER_nondet_bool();

  if (b) {
    if (c >= 'A') {
      return 1;
    } else {
      return 2;
    }
  } else {
    if (uc > 128) {
      return 3;
    } else {
      return 0;
    }
  }
}

Generated test_case_1.c:

_Bool __VERIFIER_nondet_bool(void) {
  static int i = 0;
  static const _Bool v[] = { 0 };
  return v[i++];
}

char __VERIFIER_nondet_char(void) {
  static int i = 0;
  static const char v[] = { 0 };
  return v[i++];
}

unsigned char __VERIFIER_nondet_uchar(void) {
  static int i = 0;
  static const unsigned char v[] = { 0 };
  return v[i++];
}

C++ (mixed_types.cpp):

/* Optional — esbmc_verifier.h is injected automatically at build time.*/
extern "C" {
  char __VERIFIER_nondet_char(void);
  unsigned char __VERIFIER_nondet_uchar(void);
  bool __VERIFIER_nondet_bool(void);
}

int main() {
  char c = __VERIFIER_nondet_char();
  unsigned char uc = __VERIFIER_nondet_uchar();
  bool b = __VERIFIER_nondet_bool();

  if (b) {
    if (c >= 'A') {
      return 1;
    } else {
      return 2;
    }
  } else {
    if (uc > 128) {
      return 3;
    } else {
      return 0;
    }
  }
}

Generated test_case_1.cpp:

extern "C" {

bool __VERIFIER_nondet_bool(void) {
  static int i = 0;
  static const bool v[] = { 0 };
  return v[i++];
}

char __VERIFIER_nondet_char(void) {
  static int i = 0;
  static const char v[] = { 0 };
  return v[i++];
}

unsigned char __VERIFIER_nondet_uchar(void) {
  static int i = 0;
  static const unsigned char v[] = { 0 };
  return v[i++];
}

} // extern "C"

CPP Support