CBMC
struct_encodingt Class Referencefinal

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_widthtboolbv_width
 
std::reference_wrapper< const namespacetns
 

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: