#include <custom_bitvector_analysis.h>

Inheritance diagram for custom_bitvector_domaint:

Collaboration diagram for custom_bitvector_domaint:

Classes
struct	vectorst

Public Types
typedef unsigned long long	bit_vectort

typedef std::map< irep_idt, bit_vectort >	bitst

Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett	locationt

typedef ai_history_baset::trace_ptrt	trace_ptrt

Public Member Functions
void	transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
	how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More...

void	output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override

void	make_bottom () final override
	no states More...

void	make_top () final override
	all states – the analysis doesn't use this, and domains may refuse to implement it. More...

void	make_entry () final override
	Make this domain a reasonable entry-point state. More...

bool	is_bottom () const final override

bool	is_top () const final override

bool	merge (const custom_bitvector_domaint &b, trace_ptrt from, trace_ptrt to)

void	assign_struct_rec (locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)

void	assign_lhs (const exprt &, const vectorst &)

void	assign_lhs (const irep_idt &, const vectorst &)

vectorst	get_rhs (const exprt &) const

vectorst	get_rhs (const irep_idt &) const

	custom_bitvector_domaint ()

exprt	eval (const exprt &src, custom_bitvector_analysist &) const

Public Member Functions inherited from ai_domain_baset
virtual	~ai_domain_baset ()

virtual jsont	output_json (const ai_baset &ai, const namespacet &ns) const

virtual xmlt	output_xml (const ai_baset &ai, const namespacet &ns) const

virtual bool	ai_simplify (exprt &condition, const namespacet &) const
	also add More...

virtual bool	ai_simplify_lhs (exprt &condition, const namespacet &ns) const
	Simplifies the expression but keeps it as an l-value. More...

virtual exprt	to_predicate (void) const
	Gives a Boolean condition that is true for all values represented by the domain. More...

Static Public Member Functions
static vectorst	merge (const vectorst &a, const vectorst &b)

static bool	has_get_must_or_may (const exprt &)

Public Attributes
bitst	may_bits

bitst	must_bits

tvt	has_values

Private Types
enum	modet { modet::SET_MUST, modet::CLEAR_MUST, modet::SET_MAY, modet::CLEAR_MAY }

Private Member Functions
void	set_bit (const exprt &, unsigned bit_nr, modet)

void	set_bit (const irep_idt &, unsigned bit_nr, modet)

void	erase_blank_vectors (bitst &)
	erase blank bitvectors More...

Static Private Member Functions
static void	set_bit (bit_vectort &dest, unsigned bit_nr)

static void	clear_bit (bit_vectort &dest, unsigned bit_nr)

static bool	get_bit (const bit_vectort src, unsigned bit_nr)

static irep_idt	object2id (const exprt &)

Additional Inherited Members
Protected Member Functions inherited from ai_domain_baset
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More...

	ai_domain_baset (const ai_domain_baset &old)
	A copy constructor is part of the domain interface. More...

Detailed Description

Definition at line 23 of file custom_bitvector_analysis.h.

Member Typedef Documentation

◆ bit_vectort

typedef unsigned long long custom_bitvector_domaint::bit_vectort

Definition at line 76 of file custom_bitvector_analysis.h.

◆ bitst

typedef std::map<irep_idt, bit_vectort> custom_bitvector_domaint::bitst

Definition at line 78 of file custom_bitvector_analysis.h.

Member Enumeration Documentation

◆ modet

enum custom_bitvector_domaint::modet

strongprivate

Enumerator
SET_MUST
CLEAR_MUST
SET_MAY
CLEAR_MAY

Definition at line 122 of file custom_bitvector_analysis.h.

Constructor & Destructor Documentation

◆ custom_bitvector_domaint()

custom_bitvector_domaint::custom_bitvector_domaint ( )

inline

Definition at line 112 of file custom_bitvector_analysis.h.

Member Function Documentation

◆ assign_lhs() [1/2]

void custom_bitvector_domaint::assign_lhs	(	const exprt &	lhs,
		const vectorst &	vectors
	)

Definition at line 111 of file custom_bitvector_analysis.cpp.

◆ assign_lhs() [2/2]

void custom_bitvector_domaint::assign_lhs	(	const irep_idt &	identifier,
		const vectorst &	vectors
	)

Definition at line 120 of file custom_bitvector_analysis.cpp.

◆ assign_struct_rec()

void custom_bitvector_domaint::assign_struct_rec	(	locationt	from,
		const exprt &	lhs,
		const exprt &	rhs,
		custom_bitvector_analysist &	cba,
		const namespacet &	ns
	)

Definition at line 227 of file custom_bitvector_analysis.cpp.

◆ clear_bit()

static void custom_bitvector_domaint::clear_bit	(	bit_vectort &	dest,
		unsigned	bit_nr
	)

inlinestaticprivate

Definition at line 132 of file custom_bitvector_analysis.h.

◆ erase_blank_vectors()

void custom_bitvector_domaint::erase_blank_vectors ( bitst & bits )

private

erase blank bitvectors

Definition at line 672 of file custom_bitvector_analysis.cpp.

◆ eval()

exprt custom_bitvector_domaint::eval	(	const exprt &	src,
		custom_bitvector_analysist &	custom_bitvector_analysis
	)		const

Definition at line 697 of file custom_bitvector_analysis.cpp.

◆ get_bit()

static bool custom_bitvector_domaint::get_bit	(	const bit_vectort	src,
		unsigned	bit_nr
	)

inlinestaticprivate

Definition at line 138 of file custom_bitvector_analysis.h.

◆ get_rhs() [1/2]

custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs ( const exprt & rhs ) const

Definition at line 154 of file custom_bitvector_analysis.cpp.

◆ get_rhs() [2/2]

custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs ( const irep_idt & identifier ) const

Definition at line 138 of file custom_bitvector_analysis.cpp.

◆ has_get_must_or_may()

bool custom_bitvector_domaint::has_get_must_or_may ( const exprt & src )

static

Definition at line 685 of file custom_bitvector_analysis.cpp.

◆ is_bottom()

bool custom_bitvector_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 58 of file custom_bitvector_analysis.h.

◆ is_top()

bool custom_bitvector_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 66 of file custom_bitvector_analysis.h.

◆ make_bottom()

void custom_bitvector_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 39 of file custom_bitvector_analysis.h.

◆ make_entry()

void custom_bitvector_domaint::make_entry ( )

inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 53 of file custom_bitvector_analysis.h.

◆ make_top()

void custom_bitvector_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 46 of file custom_bitvector_analysis.h.

◆ merge() [1/2]

bool custom_bitvector_domaint::merge	(	const custom_bitvector_domaint &	b,
		trace_ptrt	from,
		trace_ptrt	to
	)

Definition at line 607 of file custom_bitvector_analysis.cpp.

◆ merge() [2/2]

static vectorst custom_bitvector_domaint::merge	(	const vectorst &	a,
		const vectorst &	b
	)

inlinestatic

Definition at line 88 of file custom_bitvector_analysis.h.

◆ object2id()

irep_idt custom_bitvector_domaint::object2id ( const exprt & src )

staticprivate

Definition at line 59 of file custom_bitvector_analysis.cpp.

◆ output()

void custom_bitvector_domaint::output	(	std::ostream &	out,
		const ai_baset &	ai,
		const namespacet &	ns
	)		const

finaloverridevirtual

Reimplemented from ai_domain_baset.

Definition at line 560 of file custom_bitvector_analysis.cpp.

◆ set_bit() [1/3]

static void custom_bitvector_domaint::set_bit	(	bit_vectort &	dest,
		unsigned	bit_nr
	)

inlinestaticprivate

Definition at line 127 of file custom_bitvector_analysis.h.

◆ set_bit() [2/3]

void custom_bitvector_domaint::set_bit	(	const exprt &	lhs,
		unsigned	bit_nr,
		modet	mode
	)

private

Definition at line 49 of file custom_bitvector_analysis.cpp.

◆ set_bit() [3/3]

void custom_bitvector_domaint::set_bit	(	const irep_idt &	identifier,
		unsigned	bit_nr,
		modet	mode
	)

private

Definition at line 24 of file custom_bitvector_analysis.cpp.

◆ transform()

void custom_bitvector_domaint::transform	(	const irep_idt &	function_from,
		trace_ptrt	from,
		const irep_idt &	function_to,
		trace_ptrt	to,
		ai_baset &	ai,
		const namespacet &	ns
	)

finaloverridevirtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature

Implements ai_domain_baset.

Definition at line 269 of file custom_bitvector_analysis.cpp.

Member Data Documentation

◆ has_values

tvt custom_bitvector_domaint::has_values

Definition at line 110 of file custom_bitvector_analysis.h.

◆ may_bits

bitst custom_bitvector_domaint::may_bits

Definition at line 96 of file custom_bitvector_analysis.h.

◆ must_bits

bitst custom_bitvector_domaint::must_bits

Definition at line 96 of file custom_bitvector_analysis.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/custom_bitvector_analysis.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/custom_bitvector_analysis.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Private Types

Private Member Functions

Static Private Member Functions

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ bit_vectort

◆ bitst

Member Enumeration Documentation

◆ modet

Constructor & Destructor Documentation

◆ custom_bitvector_domaint()

Member Function Documentation

◆ assign_lhs() [1/2]

◆ assign_lhs() [2/2]

◆ assign_struct_rec()

◆ clear_bit()

◆ erase_blank_vectors()

◆ eval()

◆ get_bit()

◆ get_rhs() [1/2]

◆ get_rhs() [2/2]

◆ has_get_must_or_may()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_entry()

◆ make_top()

◆ merge() [1/2]

◆ merge() [2/2]

◆ object2id()

◆ output()

◆ set_bit() [1/3]

◆ set_bit() [2/3]

◆ set_bit() [3/3]

◆ transform()

Member Data Documentation

◆ has_values

◆ may_bits

◆ must_bits