struct_encodingt Class Reference

Encodes struct types/values into non-struct expressions/types. More...

#include <struct_encoding.h>

Collaboration diagram for struct_encodingt:

Public Member Functions
	struct_encodingt (const namespacet &ns)
	struct_encodingt (const struct_encodingt &other)
	~struct_encodingt ()
typet	encode (typet type) const
exprt	encode (exprt expr) const
exprt	decode (const exprt &encoded, const struct_tag_typet &original_type) const
	Reconstructs a struct expression of the original_type using the data from the bit vector encoded expression. More...
exprt	decode (const exprt &encoded, const union_tag_typet &original_type) const

Private Member Functions
exprt	encode_member (const member_exprt &member_expr) const
	The member expression selects the value of a field from a struct or union. More...

Private Attributes
std::unique_ptr< boolbv_widtht >	boolbv_width
std::reference_wrapper< const namespacet >	ns

Detailed Description

Encodes struct types/values into non-struct expressions/types.

Definition at line 18 of file struct_encoding.h.

Constructor & Destructor Documentation

struct_encodingt() [1/2]

struct_encodingt::struct_encodingt ( const namespacet &  ns )

explicit

Definition at line 21 of file struct_encoding.cpp.

struct_encodingt() [2/2]

struct_encodingt::struct_encodingt

(

const struct_encodingt &

other

)

Definition at line 26 of file struct_encoding.cpp.

~struct_encodingt()

struct_encodingt::~struct_encodingt ( )

default

Member Function Documentation

decode() [1/2]

exprt struct_encodingt::decode	(	const exprt &	encoded,
		const struct_tag_typet &	original_type
	)		const

Reconstructs a struct expression of the original_type using the data from the bit vector encoded expression.

Definition at line 256 of file struct_encoding.cpp.

decode() [2/2]

exprt struct_encodingt::decode	(	const exprt &	encoded,
		const union_tag_typet &	original_type
	)		const

Definition at line 284 of file struct_encoding.cpp.

encode() [1/2]

exprt struct_encodingt::encode

(

exprt

expr

)

const

Definition at line 216 of file struct_encoding.cpp.

encode() [2/2]

typet struct_encodingt::encode

(

typet

type

)

const

Definition at line 47 of file struct_encoding.cpp.

encode_member()

exprt struct_encodingt::encode_member ( const member_exprt &  member_expr ) const

private

The member expression selects the value of a field from a struct or union.

Both structs and unions are encoded into a single large bit vector. The fields of a union are encoded into the lowest bits, with padding in the highest bits if needed. Structs are encoded as a single bitvector where the first field is stored in the highest bits. The second field is stored in the next highest set of bits and so on. As offsets are indexed from the lowest bit, any field can be selected by extracting the range of bits starting from an offset based on the combined width of the fields which follow the field being selected.

Definition at line 194 of file struct_encoding.cpp.

Member Data Documentation

boolbv_width

std::unique_ptr<boolbv_widtht> struct_encodingt::boolbv_width

private

Definition at line 35 of file struct_encoding.h.

ns

std::reference_wrapper<const namespacet> struct_encodingt::ns

private

Definition at line 36 of file struct_encoding.h.

---

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

• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/encoding/struct_encoding.h
• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/encoding/struct_encoding.cpp