- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <util/lang/c_types.h>#include <irep2/irep2_expr.h>#include <irep2/simplification_check.h>#include <util/irep/migrate.h>#include <util/message/message.h>Go to the source code of this file.
Functions | |
| std::string | indent_str_irep2 (unsigned int indent) |
| bool | same_function_pointer_ignoring_argument_names (const type2tc &a, const type2tc &b) |
| bool | is_bv_type (const type2tc &t) |
| Test whether type is an integer. | |
| bool | is_bv_type (const expr2tc &e) |
| bool | is_fractional_type (const type2tc &t) |
| Test whether type is a float/double. | |
| bool | is_comparison_expr (const expr2tc &e) |
Test whether e is a relational comparison: ==, !=, <, >, <=, >=. | |
| bool | is_number_type (const type2tc &t) |
| Test whether type is a number type - bv, fixedbv or floatbv. | |
| bool | is_number_type (const expr2tc &e) |
| bool | is_scalar_type (const type2tc &t) |
| bool | is_scalar_type (const expr2tc &e) |
| bool | is_multi_dimensional_array (const type2tc &t) |
| bool | is_multi_dimensional_array (const expr2tc &e) |
| bool | is_array_or_vector_type (const type2tc &t) |
| bool | is_array_or_vector_type (const expr2tc &e) |
| const type2tc & | array_or_vector_subtype (const type2tc &t) |
| const expr2tc & | array_or_vector_size (const type2tc &t) |
| bool | array_or_vector_size_is_infinite (const type2tc &t) |
| bool | is_byte_type (const type2tc &t) |
| bool | is_byte_type (const expr2tc &e) |
| bool | is_constant_number (const expr2tc &t) |
| bool | is_constant_expr (const expr2tc &t) |
| bool | is_constant (const expr2tc &t) |
| bool | is_structure_type (const type2tc &t) |
| bool | is_structure_type (const expr2tc &e) |
| bool | is_arith_expr (const expr2tc &expr) |
| bool | is_comp_expr (const expr2tc &expr) |
| bool | is_true (const expr2tc &expr) |
| Test if expr is true. | |
| bool | is_false (const expr2tc &expr) |
| Test if expr is false. | |
| const expr2tc & | gen_true_expr () |
| const expr2tc & | gen_false_expr () |
| expr2tc | gen_long (const type2tc &type, BigInt val) |
| expr2tc | gen_ulong (BigInt v) |
| expr2tc | gen_ulong (unsigned long val) |
| const type2tc & | get_base_array_subtype (const type2tc &type) |
| bool | simplify (expr2tc &expr) |
| 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=false) |
Build the canonical zero value of type. | |
| expr2tc | gen_one (const type2tc &type) |
Build the canonical one value of type. | |
| template<typename Func> | |
| expr2tc | distribute_vector_operation (Func func, const expr2tc &op1, const expr2tc &op2) |
| Distribute the functor func over op1 and op2 at least one of those must be a vector. | |
| 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. | |
| 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::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. | |
| 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. | |
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.
|
inline |
Distribute the functor func over op1 and op2 at least one of those must be a vector.
Here, if one of the operands is nil then func must support an operation between the vector subtype and nil
| func | the functor operation e.g add, sub, mul |
| op1 | the first operand |
| op2 | the second operand |
|
inline |
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.
|
inline |
|
inline |
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 | ) |
Test whether e is a relational comparison: ==, !=, <, >, <=, >=.
Test if expr is false.
First checks whether the expr is a constant bool, and then whether it's false-valued. If these are both true, return true, otherwise return false.
| expr | Expression to check for false value. |
Test whether type is a number type - bv, fixedbv or floatbv.
Test if expr is true.
First checks whether the expr is a constant bool, and then whether it's true-valued. If these are both true, return true, otherwise return false.
| expr | Expression to check for true value. |
| 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.
1.15.0