- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <irep2/irep2_utils.h>#include <irep2/irep2_dispatch.h>#include <util/lang/c_types.h>#include <util/irep/pad_names.h>Functions | |
| void | make_not (expr2tc &expr) |
Negate expr in place. | |
| expr2tc | conjunction (std::vector< expr2tc > cs) |
Build the left-associative AND-chain of cs: and(and(and(c0, c1), c2), ...). | |
| expr2tc | disjunction (std::vector< expr2tc > cs) |
Build the left-associative OR-chain of cs. | |
| expr2tc | gen_nondet (const type2tc &type) |
Build a sideeffect2t of kind nondet of type, i.e. | |
| expr2tc | gen_zero (const type2tc &type, bool array_as_array_of) |
Build the canonical zero value of type. | |
| expr2tc | gen_one (const type2tc &type) |
Build the canonical one value of type. | |
| expr2tc | distribute_vector_operation (expr2t::expr_ids id, const expr2tc &op1, const expr2tc &op2, const expr2tc &rm) |
| Element-wise vector operation by expr_id dispatch. | |
| expr2tc | make_cmp_value (const type2tc &t, int v) |
| void | get_symbols (const expr2tc &expr, std::unordered_set< expr2tc, irep2_hash > &symbols) |
Collect every user-level symbol2t referenced by expr into symbols. | |
| std::string | indent_str_irep2 (unsigned int indent) |
| template<> | |
| bool | do_get_sub_expr< expr2tc > (const expr2tc &item, size_t idx, size_t &it, const expr2tc *&ptr) |
| template<> | |
| bool | do_get_sub_expr< std::vector< expr2tc > > (const std::vector< expr2tc > &item, size_t idx, size_t &it, const expr2tc *&ptr) |
| template<> | |
| size_t | do_count_sub_exprs< const expr2tc > (const expr2tc &) |
| template<> | |
| size_t | do_count_sub_exprs< const std::vector< expr2tc > > (const std::vector< expr2tc > &item) |
| template<> | |
| void | call_expr_delegate< const expr2tc, expr2t::const_op_delegate > (const expr2tc &ref, expr2t::const_op_delegate &f) |
| template<> | |
| void | call_expr_delegate< expr2tc, expr2t::op_delegate > (expr2tc &ref, expr2t::op_delegate &f) |
| template<> | |
| void | call_type_delegate< const type2tc, type2t::const_subtype_delegate > (const type2tc &ref, type2t::const_subtype_delegate &f) |
| template<> | |
| void | call_type_delegate< type2tc, type2t::subtype_delegate > (type2tc &ref, type2t::subtype_delegate &f) |
| std::string | type_to_string (const bool &thebool, int) |
| std::string | type_to_string (const sideeffect_allockind &data, int) |
| std::string | type_to_string (const unsigned int &theval, int) |
| std::string | type_to_string (const constant_string_kindt &theval, int) |
| std::string | type_to_string (const pointer_ref_kindt &theval, int) |
| std::string | type_to_string (const printf_kindt &theval, int) |
| std::string | type_to_string (const symbol_renaming_level &theval, int) |
| std::string | type_to_string (const BigInt &theint, int) |
| std::string | type_to_string (const fixedbvt &theval, int) |
| std::string | type_to_string (const ieee_floatt &theval, int) |
| std::string | type_to_string (const std::vector< expr2tc > &theval, int indent) |
| std::string | type_to_string (const std::vector< type2tc > &theval, int indent) |
| std::string | type_to_string (const std::vector< irep_idt > &theval, int indent) |
| std::string | type_to_string (const expr2tc &theval, int indent) |
| std::string | type_to_string (const type2tc &theval, int indent) |
| std::string | type_to_string (const irep_idt &theval, int) |
| int | do_type_lt (const BigInt &side1, const BigInt &side2) |
| int | do_type_lt (const std::vector< expr2tc > &side1, const std::vector< expr2tc > &side2) |
| int | do_type_lt (const std::vector< type2tc > &side1, const std::vector< type2tc > &side2) |
| int | do_type_lt (const expr2tc &side1, const expr2tc &side2) |
| int | do_type_lt (const type2tc &side1, const type2tc &side2) |
| std::vector< expr2tc > | pad_struct_operands (const struct_type2t &st, std::vector< expr2tc > ops) |
| Insert a zero operand at each reserved padding-member position so a struct literal's operand list matches its type's component list, exactly as clang_c_adjust::adjust_struct's insertion loop does. | |
| static expr2tc | strip_typecasts (const expr2tc &e) |
| irep_idt | quantifier_bound_name (const expr2tc &binder) |
Base name of the variable a forall2t/exists2t binds, or an empty id when binder holds no symbol at all. | |
| irep_idt | quantifier_direct_bound_name (const expr2tc &binder) |
As quantifier_bound_name, but empty unless binder is (a typecast of) address_of(symbol), i.e. | |
| void call_expr_delegate< const expr2tc, expr2t::const_op_delegate > | ( | const expr2tc & | ref, |
| expr2t::const_op_delegate & | f ) |
| void call_expr_delegate< expr2tc, expr2t::op_delegate > | ( | expr2tc & | ref, |
| expr2t::op_delegate & | f ) |
| void call_type_delegate< const type2tc, type2t::const_subtype_delegate > | ( | const type2tc & | ref, |
| type2t::const_subtype_delegate & | f ) |
| void call_type_delegate< type2tc, type2t::subtype_delegate > | ( | type2tc & | ref, |
| type2t::subtype_delegate & | f ) |
Build the left-associative AND-chain of cs: and(and(and(c0, c1), c2), ...).
Returns gen_true_expr() when the input is empty (identity for conjunction).
Build the left-associative OR-chain of cs.
Returns gen_true_expr() when the input is empty — note this is the convention used by the existing callers, not the strict identity for disjunction (which would be false). Preserves callers that short-circuit on "no constraints means trivially satisfied".
| expr2tc distribute_vector_operation | ( | expr2t::expr_ids | id, |
| const expr2tc & | op1, | ||
| const expr2tc & | op2 = expr2tc(), | ||
| const expr2tc & | rm = expr2tc() ) |
Element-wise vector operation by expr_id dispatch.
At least one of op1 / op2 must be a vector. For each lane, builds the corresponding scalar IR node (neg / add / sub / mul / div / mod / shl / bit{and,or,xor,not} / ieee_{add,sub,mul,div}). IEEE variants honour the rounding-mode operand rm; the others ignore it. Returns a fresh constant_vector2t holding the lanes. Unlike the templated overload, this form doesn't take a functor — it switches on id internally, which is convenient at frontend / migration sites that already have the expr_id at hand.
| size_t do_count_sub_exprs< const expr2tc > | ( | const expr2tc & | ) |
| size_t do_count_sub_exprs< const std::vector< expr2tc > > | ( | const std::vector< expr2tc > & | item | ) |
| bool do_get_sub_expr< expr2tc > | ( | const expr2tc & | item, |
| size_t | idx, | ||
| size_t & | it, | ||
| const expr2tc *& | ptr ) |
| bool do_get_sub_expr< std::vector< expr2tc > > | ( | const std::vector< expr2tc > & | item, |
| size_t | idx, | ||
| size_t & | it, | ||
| const expr2tc *& | ptr ) |
Build a sideeffect2t of kind nondet of type, i.e.
an expression whose value is left to the SMT solver. Used at frontend / migration boundaries to seed unspecified inputs.
Build the canonical one value of type.
Defined for bool, BV (any width), fixedbv, floatbv. Aborts on aggregate types — "one" isn't meaningful for structs/arrays/unions.
Build the canonical zero value of type.
Handles bool, BV (signed/unsigned, any width), fixedbv, floatbv, vector, array, pointer (NULL), struct (zero-of-each-member) and union (zero-of- first-member). Recursive for aggregates.
| array_as_array_of | When true, an array_type collapses to a single constant_array_of2t rather than expanding to N elements. Useful when downstream consumers prefer the run-length form. |
| void get_symbols | ( | const expr2tc & | expr, |
| std::unordered_set< expr2tc, irep2_hash > & | symbols ) |
Collect every user-level symbol2t referenced by expr into symbols.
Symbols whose name begins with "__ESBMC_" are treated as compiler internals and skipped (their subtree is not descended). Recursive — visits the expression tree via foreach_operand.
| std::string indent_str_irep2 | ( | unsigned int | indent | ) |
| void make_not | ( | expr2tc & | expr | ) |
Negate expr in place.
Folds constant true/false directly to gen_false_expr() / gen_true_expr() singletons, peels a redundant not(not(x)) to x, otherwise wraps in not2tc. The result is swapped into expr.
| std::vector< expr2tc > pad_struct_operands | ( | const struct_type2t & | st, |
| std::vector< expr2tc > | ops ) |
Insert a zero operand at each reserved padding-member position so a struct literal's operand list matches its type's component list, exactly as clang_c_adjust::adjust_struct's insertion loop does.
IREP2 carries no is_padding flag, so the member name is the signal (util/irep/pad_names.h). Idempotent: returns ops unchanged when already padded.
Base name of the variable a forall2t/exists2t binds, or an empty id when binder holds no symbol at all.
Strips typecasts, then the address_of the solver expects around a binder that names a variable directly.
A binder of any other shape yields the name of whatever symbol it does hold: void *q = &i; __ESBMC_forall(q, ...) binds i but reads as q. Callers that must not confuse the two want the strict form below.
As quantifier_bound_name, but empty unless binder is (a typecast of) address_of(symbol), i.e.
unless it names the bound variable directly.
| std::string type_to_string | ( | const constant_string_kindt & | theval, |
| int | ) |
| std::string type_to_string | ( | const ieee_floatt & | theval, |
| int | ) |
| std::string type_to_string | ( | const pointer_ref_kindt & | theval, |
| int | ) |
| std::string type_to_string | ( | const printf_kindt & | theval, |
| int | ) |
| std::string type_to_string | ( | const sideeffect_allockind & | data, |
| int | ) |
| std::string type_to_string | ( | const symbol_renaming_level & | theval, |
| int | ) |
1.15.0