fallible_calls.cpp File Reference

#include <util/lang/fallible_calls.h>
#include <cassert>
#include <irep2/irep2_utils.h>

Include dependency graph for fallible_calls.cpp:

Functions
const std::vector< fallible_call_t > &	fallible_calls ()
	Returns the immutable whitelist of fallible calls recognised by v1.
static std::string_view	strip_om_suffix (std::string_view name)
	Strip ESBMC operational-model suffixes the pthread OM uses when rewriting user-level calls (pthread_mutex_lock → pthread_mutex_lock_noassert / _nocheck, etc.).
const fallible_call_t *	find_fallible (std::string_view name)
	Looks up a fallible-call entry by unmangled function name.
expr2tc	success_predicate (success_kind kind, const expr2tc &ret_value)
	Builds the boolean expression that holds iff ret_value (typed to match the call's return type) lies in the call's success domain.

Function Documentation

fallible_calls()

const std::vector< fallible_call_t > & fallible_calls

(

)

Returns the immutable whitelist of fallible calls recognised by v1.

find_fallible()

const fallible_call_t * find_fallible

(

std::string_view

name

)

Looks up a fallible-call entry by unmangled function name.

Returns nullptr if name is not on the whitelist.

strip_om_suffix()

std::string_view strip_om_suffix ( std::string_view name )

static

Strip ESBMC operational-model suffixes the pthread OM uses when rewriting user-level calls (pthread_mutex_lock → pthread_mutex_lock_noassert / _nocheck, etc.).

Without this every pthread entry on the whitelist would be dead — the goto-program carries the suffixed name, not the C-level one. The suffix list must stay in sync with src/c2goto/library/pthread_lib.c; the fallible_calls_test Catch suite asserts every pthread_* whitelist entry resolves through both suffixes, so drift trips that test.

success_predicate()

expr2tc success_predicate	(	success_kind	kind,
		const expr2tc &	ret_value )

Builds the boolean expression that holds iff ret_value (typed to match the call's return type) lies in the call's success domain.