this file will contains helper functions for manipulating files More...

Classes
class	file_data
	Read-only contents of a file, either bundled into the ESBMC binary or read from disk. More...
class	tmp_path
	Represents a temporary path, which is (optionally) removed by the destructor. More...
class	tmp_file
	Temporary path to an open file with an associated FILE handle. More...
class	tmp_dir_override
	Points the temp directory the functions below create paths in at dir for the lifetime of this object, restoring it on destruction. More...
class	filesystemt
	Files bundled into the binary, overlaid on the real filesystem. More...

Functions
bool	is_bundled_source (std::string_view file)
	True if `file` names one of ESBMC's own operational-model or library sources rather than user code.
const std::string	get_unique_tmp_path (const std::string &format)
	Generates a unique path based on the format.
tmp_file	create_tmp_file (const std::string &format="esbmc.%%%%-%%%%-%%%%", const char *mode="w+")
	The file is created exclusively and with 0600 permissions, so it is never a pre-existing path (or a symlink to one) that this would clobber.
tmp_path	create_tmp_dir (const std::string &format="esbmc.%%%%-%%%%-%%%%")
void	create_path_and_write (const std::string &path, const char *s, size_t n)
	Creates all folders needed for a path.
void	register_tmp_for_cleanup (const std::string &path)
	The register_*() registries below are process-global, append-only and unsynchronised; each is read by the function named alongside it.
void	cleanup_registered_tmps ()
void	register_pgroup_for_cleanup (long pgid)
	Track child process groups so the signal/timeout exit paths can kill them.
void	unregister_pgroup (long pgid)
void	kill_registered_pgroups ()
void	kill_registered_pgroups_from_signal ()
	Async-signal-safe counterparts of the two cleanup calls above, for use from a signal handler.
void	remove_registered_tmps_from_signal ()

Variables
constexpr const char *	ESBMC_VFS_ROOT = "/esbmc-vfs"
	Root of the bundled path namespace, e.g.

Detailed Description

this file will contains helper functions for manipulating files

Function Documentation

◆ cleanup_registered_tmps()

void file_operations::cleanup_registered_tmps ( )

◆ create_path_and_write()

void file_operations::create_path_and_write	(	const std::string &	path,
		const char *	s,
		size_t	n )

Creates all folders needed for a path.

std::ofstream will not create folders needed for a complete path. This will generate the folder and the file contents

◆ create_tmp_dir()

tmp_path file_operations::create_tmp_dir ( const std::string & format = "esbmc.%%%%-%%%%-%%%%" )

◆ create_tmp_file()

tmp_file file_operations::create_tmp_file	(	const std::string &	format = "esbmc.%%%%-%%%%-%%%%",
		const char *	mode = "w+" )

The file is created exclusively and with 0600 permissions, so it is never a pre-existing path (or a symlink to one) that this would clobber.

◆ get_unique_tmp_path()

const std::string file_operations::get_unique_tmp_path ( const std::string & format )

Generates a unique path based on the format.

In Linux, running this function with "esbmc-%%%%" will return a string such as "/tmp/esbmc-0001" or "/tmp/esbmc-8787".

The directory is created before the path is returned, so the name is the caller's for as long as it keeps it. Unlike create_tmp_dir() the result is not registered for cleanup: the caller owns removal.

This function does not have guarantee that will finish and can be run forever until it sees an available spot.

Parameters

format A string in the file specification

◆ is_bundled_source()

bool file_operations::is_bundled_source ( std::string_view file )

True if file names one of ESBMC's own operational-model or library sources rather than user code.

◆ kill_registered_pgroups()

void file_operations::kill_registered_pgroups ( )

◆ kill_registered_pgroups_from_signal()

void file_operations::kill_registered_pgroups_from_signal ( )

Async-signal-safe counterparts of the two cleanup calls above, for use from a signal handler.

The ordinary versions walk std:: containers and, for the temporaries, run boost::filesystem::remove_all; both allocate, so a handler interrupting the allocator deadlocks or trips glibc's heap assertion (#6201). These read fixed-capacity mirrors populated at registration time and call nothing outside POSIX's async-signal-safe set. Neither clears the mirror: a handler runs once, on the way to _exit().

◆ register_pgroup_for_cleanup()

void file_operations::register_pgroup_for_cleanup ( long pgid )

Track child process groups so the signal/timeout exit paths can kill them.

A backend that spawns an external solver into its own process group (so the group can be killed as a unit, MPI ranks included) registers the pgid here. On a timeout or fatal signal ESBMC exits without running destructors; kill_registered_pgroups(), called from those handlers, sends SIGKILL to each still-registered group so the children do not linger. unregister_pgroup() is called once the child has been reaped normally. No-op on Windows. pgid is a pid_t widened to long to keep this header POSIX-free.

◆ register_tmp_for_cleanup()

void file_operations::register_tmp_for_cleanup ( const std::string & path )

The register_*() registries below are process-global, append-only and unsynchronised; each is read by the function named alongside it.

A signal landing mid-append can observe a half-written registry.

Temporary paths, read by cleanup_registered_tmps() from the signal handlers, which run before exit() reaches any destructor.

◆ remove_registered_tmps_from_signal()

void file_operations::remove_registered_tmps_from_signal ( )

◆ unregister_pgroup()

void file_operations::unregister_pgroup ( long pgid )

Variable Documentation

◆ ESBMC_VFS_ROOT

const char* file_operations::ESBMC_VFS_ROOT = "/esbmc-vfs"

inlineconstexpr

Root of the bundled path namespace, e.g.

/esbmc-vfs/clang/include. Reserved, so it never names anything on the real filesystem.

Classes

Functions

Variables