ctest_generator Class Reference

This generates CTest test-cases for C programs. More...

#include <ctest.h>

Public Member Functions
	ctest_generator ()=default
void	clear ()
	Clear collected data (called at start of coverage run).
void	collect (const symex_target_equationt &target, smt_convt &smt_conv, const namespacet &ns)
	Collect test data from a counterexample (called for each CEX in coverage mode).
void	generate (const std::string &output_dir) const
	Generate C test files and CMakeLists.txt from collected data into output_dir.
void	generate_single (const std::string &output_dir, const symex_target_equationt &target, smt_convt &smt_conv, const namespacet &ns)
	Single-shot generation for non-coverage mode.
bool	has_tests () const
	Check if any test cases have been collected.

Static Public Attributes
static constexpr const char *	default_output_dir = "esbmc-ctest"
	Output goes to a dedicated subdirectory: writing into the working directory silently destroyed files ESBMC did not own (github #6214).

Detailed Description

This generates CTest test-cases for C programs.

Constructor & Destructor Documentation

ctest_generator()

ctest_generator::ctest_generator ( )

default

Member Function Documentation

clear()

void ctest_generator::clear

(

)

Clear collected data (called at start of coverage run).

collect()

void ctest_generator::collect	(	const symex_target_equationt &	target,
		smt_convt &	smt_conv,
		const namespacet &	ns )

Collect test data from a counterexample (called for each CEX in coverage mode).

generate()

void ctest_generator::generate

(

const std::string &

output_dir

)

const

Generate C test files and CMakeLists.txt from collected data into output_dir.

Refuses to overwrite files ESBMC did not generate.

generate_single()

void ctest_generator::generate_single	(	const std::string &	output_dir,
		const symex_target_equationt &	target,
		smt_convt &	smt_conv,
		const namespacet &	ns )

Single-shot generation for non-coverage mode.

has_tests()

bool ctest_generator::has_tests

(

)

const

Check if any test cases have been collected.

Member Data Documentation

default_output_dir

const char* ctest_generator::default_output_dir = "esbmc-ctest"

staticconstexpr

Output goes to a dedicated subdirectory: writing into the working directory silently destroyed files ESBMC did not own (github #6214).

---

The documentation for this class was generated from the following files:

• src/goto-symex/testgen/ctest.h
• src/goto-symex/testgen/ctest.cpp