C/C++ CTest Test Case Generation

Documentation

C and C++

Overview

ESBMC supports the automatic generation of CTest branch-coverage test cases for C and C++ programs.

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

This will 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++.

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

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