C CTest Test Case Generation

Documentation

C and C++

Overview

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

Dependencies

CMake (includes CTest)
Clang
LLVM tools (llvm-cov)
gcov and gcovr

Usage

Basic Command

Generate multiple test cases (branch coverage mode)

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

This will generate:

test_case.c (or test_case_1.c, test_case_2.c, …) - Test case implementations
CMakeLists.txt - CMake build configuration

Input Format

Your C code should use __VERIFIER_nondet_*() functions to mark symbolic inputs(Consistent with SV-COMP):

// 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;
}

Output Format

ESBMC will generate test case implementations. Each test_case_i.c only provides concrete implementations of __VERIFIER_nondet_* and must not define main() :

test_case.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++];
}

CMakeLists.txt:

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

add_executable(test_case_2 example.c test_case_2.c)
add_test(NAME test_case_2 COMMAND test_case_2)

add_executable(test_case_3 example.c test_case_3.c)
add_test(NAME test_case_3 COMMAND test_case_3)

add_executable(test_case_4 example.c test_case_4.c)
add_test(NAME test_case_4 COMMAND test_case_4)

add_executable(test_case_5 example.c test_case_5.c)
add_test(NAME test_case_5 COMMAND test_case_5)

add_executable(test_case_6 example.c test_case_6.c)
add_test(NAME test_case_6 COMMAND test_case_6)

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

gcovr -r .. --branches --object-directory . --gcov-executable "llvm-cov gcov"

Note: if you don’t have gcovr installed on your machine, you can run the command:

sudo apt 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    --%
test_case_2.c                                  0       0    --%
test_case_3.c                                  0       0    --%
test_case_4.c                                  0       0    --%
test_case_5.c                                  0       0    --%
test_case_6.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 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	Standard	Example Values
`__VERIFIER_nondet_bool()`	`_Bool`	C99/SV-COMP	`0, 1`

Example: Multiple Types

// 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.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++];
}

CPP Support