CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
struct_encoding.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
5
6#include <util/expr.h> // For passing exprt by value. // IWYU pragma: keep
7#include <util/type.h> // For passing `typet` by value. // IWYU pragma: keep
8
9#include <memory>
10
11class namespacet;
12class boolbv_widtht;
13class member_exprt;
15class union_tag_typet;
16
19{
20public:
21 explicit struct_encodingt(const namespacet &ns);
24
25 typet encode(typet type) const;
26 exprt encode(exprt expr) const;
29 exprt
31 exprt
32 decode(const exprt &encoded, const union_tag_typet &original_type) const;
33
34private:
35 std::unique_ptr<boolbv_widtht> boolbv_width;
36 std::reference_wrapper<const namespacet> ns;
37
39};
40
41#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
Extract member of struct or union.
Definition std_expr.h:2971
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Encodes struct types/values into non-struct expressions/types.
std::unique_ptr< boolbv_widtht > boolbv_width
std::reference_wrapper< const namespacet > ns
typet encode(typet type) 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 expr...
exprt encode_member(const member_exprt &member_expr) const
The member expression selects the value of a field from a struct or union.
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
The type of an expression, extends irept.
Definition type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
Defines typet, type_with_subtypet and type_with_subtypest.