CBMC
|
#include "simplify_utils.h"
#include "arith_tools.h"
#include "c_types.h"
#include "config.h"
#include "endianness_map.h"
#include "expr_util.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "pointer_offset_size.h"
#include "std_expr.h"
#include "string_constant.h"
#include "symbol.h"
#include <algorithm>
Go to the source code of this file.
Classes | |
struct | saj_tablet |
produce canonical ordering for associative and commutative binary operators More... | |
Functions | |
bool | sort_operands (exprt::operandst &operands) |
sort operands of an expression according to ordering defined by operator< | |
static bool | is_associative_and_commutative_for_type (const struct saj_tablet &saj_entry, const irep_idt &type_id) |
static const struct saj_tablet & | get_sort_and_join_table_entry (const irep_idt &id, const irep_idt &type_id) |
static bool | sort_and_join (exprt &expr, bool do_sort) |
bool | sort_and_join (exprt &expr) |
bool | join_operands (exprt &expr) |
std::optional< exprt > | bits2expr (const std::string &bits, const typet &type, bool little_endian, const namespacet &ns) |
std::optional< std::string > | expr2bits (const exprt &expr, bool little_endian, const namespacet &ns) |
std::optional< std::reference_wrapper< const array_exprt > > | try_get_string_data_array (const exprt &content, const namespacet &ns) |
Get char sequence from content field of a refined string expression. | |
Variables | |
struct saj_tablet | saj_table [] |
std::optional< exprt > bits2expr | ( | const std::string & | bits, |
const typet & | type, | ||
bool | little_endian, | ||
const namespacet & | ns | ||
) |
Definition at line 196 of file simplify_utils.cpp.
std::optional< std::string > expr2bits | ( | const exprt & | expr, |
bool | little_endian, | ||
const namespacet & | ns | ||
) |
Definition at line 414 of file simplify_utils.cpp.
|
static |
Definition at line 121 of file simplify_utils.cpp.
|
static |
Definition at line 109 of file simplify_utils.cpp.
Definition at line 191 of file simplify_utils.cpp.
Definition at line 186 of file simplify_utils.cpp.
Definition at line 136 of file simplify_utils.cpp.
bool sort_operands | ( | exprt::operandst & | operands | ) |
sort operands of an expression according to ordering defined by operator<
Definition at line 28 of file simplify_utils.cpp.
std::optional< std::reference_wrapper< const array_exprt > > try_get_string_data_array | ( | const exprt & | content, |
const namespacet & | ns | ||
) |
Get char sequence from content field of a refined string expression.
If content
is of the form &id[e]
, where id
is an array-typed symbol expression (and e
is any expression), return the value of the symbol id
(as given by the value
field of the symbol in the namespace ns
); otherwise return an empty optional.
content | content field of a refined string expression |
ns | namespace |
Definition at line 489 of file simplify_utils.cpp.
struct saj_tablet saj_table[] |