#include <axioms.h>

Collaboration diagram for axiomst:

Public Member Functions
	axiomst (decision_proceduret &__dest, const std::unordered_set< symbol_exprt, irep_hash > &__address_taken, bool __verbose, const namespacet &__ns)

void	set_to_true (exprt)

void	set_to_false (exprt)

void	emit ()

exprt	translate (exprt) const

Protected Member Functions
exprt	replace (exprt)

typet	replace (typet)

void	node (const exprt &)

void	add (const state_ok_exprt &)

void	ok_fc ()

void	evaluate_fc ()

void	add (const state_is_cstring_exprt &, bool recursive)

void	is_cstring_fc ()

void	is_dynamic_object_fc ()

void	live_object ()

void	live_object_fc ()

void	writeable_object ()

void	writeable_object_fc ()

void	object_size ()

void	object_size_fc ()

void	is_sentinel_dll ()

void	initial_state ()

Protected Attributes
decision_proceduret &	dest

const std::unordered_set< symbol_exprt, irep_hash > &	address_taken

bool	verbose = false

const namespacet &	ns

std::vector< exprt >	constraints

std::unordered_map< exprt, symbol_exprt, irep_hash >	replacement_map

std::map< irep_idt, std::size_t >	counters

std::set< address_of_exprt >	address_of_exprs

std::set< object_address_exprt >	object_address_exprs

std::set< state_ok_exprt >	ok_exprs

std::set< evaluate_exprt >	evaluate_exprs

std::set< state_is_cstring_exprt >	is_cstring_exprs

std::set< state_is_dynamic_object_exprt >	is_dynamic_object_exprs

std::set< state_live_object_exprt >	live_object_exprs

std::set< state_writeable_object_exprt >	writeable_object_exprs

std::set< state_object_size_exprt >	object_size_exprs

std::set< state_is_sentinel_dll_exprt >	is_sentinel_dll_exprs

std::set< initial_state_exprt >	initial_state_exprs

Detailed Description

Definition at line 28 of file axioms.h.

Constructor & Destructor Documentation

◆ axiomst()

axiomst::axiomst	(	decision_proceduret &	__dest,
		const std::unordered_set< symbol_exprt, irep_hash > &	__address_taken,
		bool	__verbose,
		const namespacet &	__ns
	)

inline

Definition at line 31 of file axioms.h.

Member Function Documentation

◆ add() [1/2]

void axiomst::add	(	const state_is_cstring_exprt &	is_cstring_expr,
		bool	recursive
	)

protected

Definition at line 700 of file axioms.cpp.

◆ add() [2/2]

void axiomst::add ( const state_ok_exprt & ok_expr )

protected

Definition at line 628 of file axioms.cpp.

◆ emit()

void axiomst::emit ( )

Definition at line 749 of file axioms.cpp.

◆ evaluate_fc()

void axiomst::evaluate_fc ( )

protected

Definition at line 58 of file axioms.cpp.

◆ initial_state()

void axiomst::initial_state ( )

protected

Definition at line 324 of file axioms.cpp.

◆ is_cstring_fc()

void axiomst::is_cstring_fc ( )

protected

Definition at line 85 of file axioms.cpp.

◆ is_dynamic_object_fc()

void axiomst::is_dynamic_object_fc ( )

protected

Definition at line 219 of file axioms.cpp.

◆ is_sentinel_dll()

void axiomst::is_sentinel_dll ( )

protected

◆ live_object()

void axiomst::live_object ( )

protected

Definition at line 108 of file axioms.cpp.

◆ live_object_fc()

void axiomst::live_object_fc ( )

protected

Definition at line 126 of file axioms.cpp.

◆ node()

void axiomst::node ( const exprt & src )

protected

Definition at line 399 of file axioms.cpp.

◆ object_size()

void axiomst::object_size ( )

protected

Definition at line 241 of file axioms.cpp.

◆ object_size_fc()

void axiomst::object_size_fc ( )

protected

Definition at line 278 of file axioms.cpp.

◆ ok_fc()

void axiomst::ok_fc ( )

protected

Definition at line 298 of file axioms.cpp.

◆ replace() [1/2]

exprt axiomst::replace ( exprt src )

protected

Definition at line 359 of file axioms.cpp.

◆ replace() [2/2]

typet axiomst::replace ( typet src )

protected

Definition at line 39 of file axioms.cpp.

◆ set_to_false()

void axiomst::set_to_false ( exprt src )

Definition at line 34 of file axioms.cpp.

◆ set_to_true()

void axiomst::set_to_true ( exprt src )

Definition at line 29 of file axioms.cpp.

◆ translate()

exprt axiomst::translate ( exprt src ) const

Definition at line 350 of file axioms.cpp.

◆ writeable_object()

void axiomst::writeable_object ( )

protected

Definition at line 146 of file axioms.cpp.

◆ writeable_object_fc()

void axiomst::writeable_object_fc ( )

protected

Definition at line 197 of file axioms.cpp.

Member Data Documentation

◆ address_of_exprs

std::set<address_of_exprt> axiomst::address_of_exprs

protected

Definition at line 61 of file axioms.h.

◆ address_taken

const std::unordered_set<symbol_exprt, irep_hash>& axiomst::address_taken

protected

Definition at line 48 of file axioms.h.

◆ constraints

std::vector<exprt> axiomst::constraints

protected

Definition at line 52 of file axioms.h.

◆ counters

std::map<irep_idt, std::size_t> axiomst::counters

protected

Definition at line 57 of file axioms.h.

◆ dest

decision_proceduret& axiomst::dest

protected

Definition at line 47 of file axioms.h.

◆ evaluate_exprs

std::set<evaluate_exprt> axiomst::evaluate_exprs

protected

Definition at line 69 of file axioms.h.

◆ initial_state_exprs

std::set<initial_state_exprt> axiomst::initial_state_exprs

protected

Definition at line 94 of file axioms.h.

◆ is_cstring_exprs

std::set<state_is_cstring_exprt> axiomst::is_cstring_exprs

protected

Definition at line 72 of file axioms.h.

◆ is_dynamic_object_exprs

std::set<state_is_dynamic_object_exprt> axiomst::is_dynamic_object_exprs

protected

Definition at line 76 of file axioms.h.

◆ is_sentinel_dll_exprs

std::set<state_is_sentinel_dll_exprt> axiomst::is_sentinel_dll_exprs

protected

Definition at line 91 of file axioms.h.

◆ live_object_exprs

std::set<state_live_object_exprt> axiomst::live_object_exprs

protected

Definition at line 79 of file axioms.h.

◆ ns

const namespacet& axiomst::ns

protected

Definition at line 50 of file axioms.h.

◆ object_address_exprs

std::set<object_address_exprt> axiomst::object_address_exprs

protected

Definition at line 63 of file axioms.h.

◆ object_size_exprs

std::set<state_object_size_exprt> axiomst::object_size_exprs

protected

Definition at line 87 of file axioms.h.

◆ ok_exprs

std::set<state_ok_exprt> axiomst::ok_exprs

protected

Definition at line 65 of file axioms.h.

◆ replacement_map

std::unordered_map<exprt, symbol_exprt, irep_hash> axiomst::replacement_map

protected

Definition at line 56 of file axioms.h.

◆ verbose

bool axiomst::verbose = false

protected

Definition at line 49 of file axioms.h.

◆ writeable_object_exprs

std::set<state_writeable_object_exprt> axiomst::writeable_object_exprs

protected

Definition at line 83 of file axioms.h.

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

/home/runner/work/cbmc/cbmc/src/cprover/axioms.h
/home/runner/work/cbmc/cbmc/src/cprover/axioms.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ axiomst()

Member Function Documentation

◆ add() [1/2]

◆ add() [2/2]

◆ emit()

◆ evaluate_fc()

◆ initial_state()

◆ is_cstring_fc()

◆ is_dynamic_object_fc()

◆ is_sentinel_dll()

◆ live_object()

◆ live_object_fc()

◆ node()

◆ object_size()

◆ object_size_fc()

◆ ok_fc()

◆ replace() [1/2]

◆ replace() [2/2]

◆ set_to_false()

◆ set_to_true()

◆ translate()

◆ writeable_object()

◆ writeable_object_fc()

Member Data Documentation

◆ address_of_exprs

◆ address_taken

◆ constraints

◆ counters

◆ dest

◆ evaluate_exprs

◆ initial_state_exprs

◆ is_cstring_exprs

◆ is_dynamic_object_exprs

◆ is_sentinel_dll_exprs

◆ live_object_exprs

◆ ns

◆ object_address_exprs

◆ object_size_exprs

◆ ok_exprs

◆ replacement_map

◆ verbose

◆ writeable_object_exprs