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

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 __VERIFIER_nondet_*() functions to mark symbolic inputs (consistent with SV-COMP). For C++, declare them with extern "C" linkage:

C (example.c):

#include <stdio.h>

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);

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().

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)
...

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)
...

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>

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):

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