CBMC
|
#include "struct_encoding.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include <solvers/flattening/boolbv_width.h>
#include <solvers/smt2_incremental/encoding/nondet_padding.h>
#include <algorithm>
#include <numeric>
#include <optional>
#include <queue>
Go to the source code of this file.
Functions | |
static std::optional< std::size_t > | needs_width (const typet &type, const boolbv_widtht &boolbv_width) |
If the given type needs re-encoding as a bit-vector then this function. | |
static std::unordered_map< irep_idt, exprt > | extricate_updates (const with_exprt &struct_expr) |
Extracts the component/field names and new values from a with_exprt which expresses a new struct value where one or more members of a struct have had their values substituted with new values. | |
static exprt | encode (const with_exprt &with, const namespacet &ns) |
static exprt | empty_encoding () |
Empty structs and unions are encoded as a zero byte. | |
static exprt | encode (const struct_exprt &struct_expr) |
Structs are flattened into a large bit vector using concatenation to express all the member operands of struct_expr . | |
static exprt | encode (const union_exprt &union_expr, const boolbv_widtht &bit_width) |
static std::size_t | count_trailing_bit_width (const struct_typet &type, const irep_idt name, const boolbv_widtht &boolbv_width) |
|
static |
Definition at line 162 of file struct_encoding.cpp.
Empty structs and unions are encoded as a zero byte.
This has useful properties such as -
Definition at line 129 of file struct_encoding.cpp.
|
static |
Structs are flattened into a large bit vector using concatenation to express all the member operands of struct_expr
.
Definition at line 137 of file struct_encoding.cpp.
|
static |
Definition at line 147 of file struct_encoding.cpp.
|
static |
Definition at line 105 of file struct_encoding.cpp.
|
static |
Extracts the component/field names and new values from a with_exprt
which expresses a new struct value where one or more members of a struct have had their values substituted with new values.
with_exprt
only supports a single where
/ new_value
pair and does not support extracting the name from the where
operand. Definition at line 82 of file struct_encoding.cpp.
|
static |
If the given type
needs re-encoding as a bit-vector then this function.
boolbv_width
. Definition at line 38 of file struct_encoding.cpp.