|
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>
Include dependency graph for simplify_utils.cpp: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[] |