#include <util/message/message.h>
#include <filesystem>
#include <fstream>
#include <string>
#include <vector>

Include dependency graph for test_gen_guard.h:

This graph shows which files directly or indirectly include this file:

Enumerations
enum class	overwrite_verdict { safe , foreign , unreadable }

Functions
overwrite_verdict	classify_existing (const std::filesystem::path &path)
	An empty file is safe: a run killed mid-write leaves exactly that, and refusing it would wedge generation permanently over a file with nothing in it to lose.
bool	can_write_all (const std::vector< std::filesystem::path > &paths, const std::string &option_name)
	Checked up-front for every target path rather than per-file: refusing halfway through would leave a half-written project behind, which is worse than either writing all of it or none of it.

Variables
constexpr char	ESBMC_GENERATED_MARKER [] = "Auto-generated by ESBMC"
	Shared no-clobber guard for the test-case generators (CTest, pytest, ...): every file they write carries this on its first line, so an existing file without it belongs to the user (github #6214, #6220).

Enumeration Type Documentation

◆ overwrite_verdict

enum class overwrite_verdict

strong

Enumerator
safe
foreign
unreadable

Function Documentation

◆ can_write_all()

bool can_write_all	(	const std::vector< std::filesystem::path > &	paths,
		const std::string &	option_name )

inline

Checked up-front for every target path rather than per-file: refusing halfway through would leave a half-written project behind, which is worse than either writing all of it or none of it.

option_name is the command-line flag the error message suggests (e.g. "--ctest-output-dir", "--pytest-output-dir").

This check is advisory, not atomic: nothing stops the target files being created between here and the writes each caller performs afterward. That is an acceptable trade-off for a single-shot CLI writing into a directory the user controls.

◆ classify_existing()

overwrite_verdict classify_existing ( const std::filesystem::path & path )

inline

An empty file is safe: a run killed mid-write leaves exactly that, and refusing it would wedge generation permanently over a file with nothing in it to lose.

Variable Documentation

◆ ESBMC_GENERATED_MARKER

char ESBMC_GENERATED_MARKER[] = "Auto-generated by ESBMC"

inlineconstexpr

Shared no-clobber guard for the test-case generators (CTest, pytest, ...): every file they write carries this on its first line, so an existing file without it belongs to the user (github #6214, #6220).

Enumerations

Functions