- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <util/config/config.h>#include <util/lang/c_types.h>#include <util/arith/fixedbv.h>#include <util/arith/ieee_float.h>#include <util/irep/location.h>#include <irep2/irep2_type.h>#include <irep2/expr_kinds.inc>Go to the source code of this file.
Classes | |
| class | exists2t |
| class | forall2t |
| class | constant_int2t |
| Constant integer class. More... | |
| class | constant_fixedbv2t |
| Constant fixedbv class. More... | |
| class | constant_floatbv2t |
| Constant floatbv class. More... | |
| class | constant_bool2t |
| Constant boolean value. More... | |
| class | constant_string2t |
| Constant class for string constants. More... | |
| class | constant_struct2t |
| Constant structure. More... | |
| class | constant_union2t |
| Constant union expression. More... | |
| class | constant_array2t |
| Constant array. More... | |
| class | constant_vector2t |
| Constant vector. More... | |
| class | constant_array_of2t |
| Constant array of one particular value. More... | |
| class | symbol2t |
| Symbol type. More... | |
| class | nearbyint2t |
| Nearbyint expression. More... | |
| class | typecast2t |
| Typecast expression. More... | |
| class | bitcast2t |
| Bitcast expression. More... | |
| class | if2t |
| If-then-else expression. More... | |
| class | code_decl2t |
| code_decl2t — variable declaration, with optional initializer. More... | |
| class | cmp_three_way2t |
| C++20 three-way comparison a <=> b. More... | |
| class | not2t |
| Not operation. More... | |
| class | ieee_fma2t |
| IEEE fused multiply-add operation. More... | |
| class | ieee_sqrt2t |
| IEEE sqrt operation. More... | |
| class | same_object2t |
| Same-object operation. More... | |
| class | pointer_offset2t |
| Extract pointer offset. More... | |
| class | address_of2t |
| Address of operation. More... | |
| class | byte_extract2t |
| Extract byte from data. More... | |
| class | byte_update2t |
| Update byte. More... | |
| class | with2t |
| With operation. More... | |
| class | member2t |
| Member operation. More... | |
| class | member_ref2t |
| Member reference. More... | |
| class | ptr_mem2t |
| Member pointer. More... | |
| class | index2t |
| Array index operation. More... | |
| class | overflow2t |
| Check whether operand overflows. More... | |
| class | overflow_cast2t |
| Test if a cast overflows. More... | |
| class | overflow_neg2t |
| Test for negation overflows. More... | |
| class | dynamic_object2t |
| Record a dynamicly allocated object. More... | |
| class | dereference2t |
| Dereference operation. More... | |
| class | sideeffect2t |
| Irep for various side effects. More... | |
| class | code_block2t |
| class | code_assign2t |
| class | code_printf2t |
| class | code_skip2t |
| class | new_object2t |
| C++ constructor "this" placeholder (exprt("new_object")). More... | |
| class | uninterpreted_func2t |
| Uninterpreted-function application. More... | |
| class | code_goto2t |
| class | object_descriptor2t |
| class | code_function_call2t |
| class | code_ifthenelse2t |
| class | code_while2t |
| class | code_dowhile2t |
| class | code_for2t |
| class | code_switch2t |
| class | code_break2t |
| class | code_continue2t |
| class | code_label2t |
| class | code_switch_case2t |
| V.4.2: one case/default arm of a switch body. More... | |
| class | code_assert2t |
| V.4.3: code_assert / code_assume — single-guard code kinds emitted by the Python / C++ frontends for assert and __ESBMC_assume. More... | |
| class | code_assume2t |
| class | sideeffect_assign2t |
| V.4.2: wraps C-frontend sideeffect assignment nodes — simple = and compound +=, -=, etc. More... | |
| class | code_comma2t |
| class | invalid_pointer2t |
| class | code_asm2t |
| class | code_cpp_catch2t |
| class | code_cpp_throw2t |
| class | concat2t |
| Bit concatenation of two operands. More... | |
| class | extract2t |
| class | sizeof2t |
| sizeof(T) expression. More... | |
Macros | |
| #define | IREP2_EXPR(kind, pretty) |
| #define | irep_typedefs(basename) |
| #define | ESBMC_DEFINE_RELATION2T(name) |
| Defines one of the six binary boolean relation nodes. | |
| #define | ESBMC_DEFINE_ARITH_2OP(name) |
| Arithmetic two-operand node (add/sub/mul/div/modulus). | |
| #define | ESBMC_DEFINE_BIT_2OP(name) |
| Bitwise / shift two-operand node (bitand/bitor/bitxor/ shl/ashr/lshr). | |
| #define | ESBMC_DEFINE_ARITH_1OP(name) |
| Arithmetic one-operand node (neg/abs/bswap/bitnot). | |
| #define | ESBMC_DEFINE_POINTER_1OP(name) |
| Pointer one-operand node (pointer_object/pointer_capability). | |
| #define | ESBMC_DEFINE_LOGIC_2OP(name) |
| Logical two-operand boolean-result node. | |
| #define | ESBMC_DEFINE_FP_PREDICATE_1OP(name) |
| FP classification single-operand predicate (isnan/isinf/ isnormal/isfinite). | |
| #define | ESBMC_DEFINE_OBJECT_PREDICATE_1OP(name) |
| Pointer-object boolean predicate (valid_object/races_check/ deallocated_obj). | |
| #define | ESBMC_DEFINE_OBJECT_SIZE_1OP(name) |
| Pointer-object size-returning op (capability_base/capability_top/ dynamic_size). | |
| #define | ESBMC_DEFINE_OVERFLOW_INT32_1OP(name) |
| Single-operand overflow-family op returning int32 (signbit/ popcount). | |
| #define | ESBMC_DEFINE_TYPE_ONLY(name) |
| Marker node holding only a type (no operands). | |
| #define | ESBMC_DEFINE_CODE_EXPRESSION_1OP(name) |
| code_* statement with empty type and a single expr2tc operand (code_expression/code_return/code_free/code_cpp_del_array/ code_cpp_delete). | |
| #define | ESBMC_DEFINE_CODE_DECL(name) |
| code_* declaration carrying (type, irep_idt name). | |
| #define | ESBMC_DEFINE_IEEE_ARITH_2OP(name) |
| Defines an IEEE two-operand floating-point arithmetic node (add/sub/mul/div). | |
| #define | expr_macros(name) |
| #define | IREP2_EXPR(kind, pretty) |
Enumerations | |
| enum class | constant_string_kindt { DEFAULT , WIDE , UNICODE } |
| enum class | symbol_renaming_level { level0 , level1 , level2 , level1_global , level2_global } |
| Symex renaming level for symbol2t. More... | |
| enum class | sideeffect_allockind { malloc , realloc , alloca , cpp_new , cpp_new_arr , nondet , va_arg , printf2 , function_call , preincrement , postincrement , predecrement , postdecrement , old_snapshot , assigns_target , statement_expression , temporary_object , gcc_conditional_expression , cpp_delete , cpp_delete_array } |
| Enumeration identifying each particular kind of side effect. More... | |
| enum class | printf_kindt { PRINTF , FPRINTF , DPRINTF , SPRINTF , VFPRINTF , SNPRINTF , VPRINTF , VSPRINTF , VSNPRINTF , ASPRINTF , VASPRINTF } |
| Which member of the printf family a code_printf2t represents. More... | |
| #define ESBMC_DEFINE_ARITH_1OP | ( | name | ) |
| #define ESBMC_DEFINE_ARITH_2OP | ( | name | ) |
| #define ESBMC_DEFINE_BIT_2OP | ( | name | ) |
Bitwise / shift two-operand node (bitand/bitor/bitxor/ shl/ashr/lshr).
| #define ESBMC_DEFINE_CODE_DECL | ( | name | ) |
code_* declaration carrying (type, irep_idt name).
Used for code_dead. (code_decl2t is defined separately below because it also carries an initializer.)
| #define ESBMC_DEFINE_CODE_EXPRESSION_1OP | ( | name | ) |
code_* statement with empty type and a single expr2tc operand (code_expression/code_return/code_free/code_cpp_del_array/ code_cpp_delete).
| #define ESBMC_DEFINE_FP_PREDICATE_1OP | ( | name | ) |
FP classification single-operand predicate (isnan/isinf/ isnormal/isfinite).
Implicit get_bool_type() result.
| #define ESBMC_DEFINE_IEEE_ARITH_2OP | ( | name | ) |
Defines an IEEE two-operand floating-point arithmetic node (add/sub/mul/div).
Each takes two operands and a rounding mode, has matching floatbv operand/result types, and provides an out-of-line do_simplify override in src/util/expr_simplifier.cpp.
| #define ESBMC_DEFINE_LOGIC_2OP | ( | name | ) |
Logical two-operand boolean-result node.
Used for and/or/xor/ implies and the Python runtime predicates isinstance/hasattr/ isnone. Implicit get_bool_type() result.
| #define ESBMC_DEFINE_OBJECT_PREDICATE_1OP | ( | name | ) |
Pointer-object boolean predicate (valid_object/races_check/ deallocated_obj).
Implicit get_bool_type() result.
| #define ESBMC_DEFINE_OBJECT_SIZE_1OP | ( | name | ) |
Pointer-object size-returning op (capability_base/capability_top/ dynamic_size).
Implicit size_type2() result.
| #define ESBMC_DEFINE_OVERFLOW_INT32_1OP | ( | name | ) |
Single-operand overflow-family op returning int32 (signbit/ popcount).
| #define ESBMC_DEFINE_POINTER_1OP | ( | name | ) |
Pointer one-operand node (pointer_object/pointer_capability).
| #define ESBMC_DEFINE_RELATION2T | ( | name | ) |
Defines one of the six binary boolean relation nodes.
Each takes two operands of any matching scalar/pointer type, has boolean result type, and provides an out-of-line do_simplify override in src/util/expr_simplifier.cpp.
| #define ESBMC_DEFINE_TYPE_ONLY | ( | name | ) |
Marker node holding only a type (no operands).
Used for unknown/invalid/null_object.
| #define expr_macros | ( | name | ) |
| #define IREP2_EXPR | ( | kind, | |
| pretty ) |
| #define IREP2_EXPR | ( | kind, | |
| pretty ) |
| #define irep_typedefs | ( | basename | ) |
|
strong |
|
strong |
Which member of the printf family a code_printf2t represents.
| Enumerator | |
|---|---|
| PRINTF | |
| FPRINTF | |
| DPRINTF | |
| SPRINTF | |
| VFPRINTF | |
| SNPRINTF | |
| VPRINTF | |
| VSPRINTF | |
| VSNPRINTF | |
| ASPRINTF | |
| VASPRINTF | |
|
strong |
Enumeration identifying each particular kind of side effect.
|
strong |
Symex renaming level for symbol2t.
Symbolic execution rewrites a symbol into successively more specific variants as it threads constraints through the SSA program:
See src/goto-symex/state/renaming.cpp for the exact transitions.
| Enumerator | |
|---|---|
| level0 | |
| level1 | |
| level2 | |
| level1_global | |
| level2_global | |
| void assert_arith_2ops_consistency | ( | const type2tc & | t, |
| expr2t::expr_ids | id, | ||
| const expr2tc & | v1, | ||
| const expr2tc & | v2 ) |
Debug-only consistency check for arith_2ops operands and result type.
Called from add2t/sub2t/mul2t/div2t/modulus2t constructors; no-op in Release.
| ESBMC_DEFINE_ARITH_1OP | ( | abs | ) |
| ESBMC_DEFINE_ARITH_1OP | ( | bitnot | ) |
| ESBMC_DEFINE_ARITH_1OP | ( | bswap | ) |
| ESBMC_DEFINE_ARITH_1OP | ( | neg | ) |
| ESBMC_DEFINE_ARITH_2OP | ( | add | ) |
| ESBMC_DEFINE_ARITH_2OP | ( | div | ) |
| ESBMC_DEFINE_ARITH_2OP | ( | modulus | ) |
| ESBMC_DEFINE_ARITH_2OP | ( | mul | ) |
| ESBMC_DEFINE_ARITH_2OP | ( | sub | ) |
| ESBMC_DEFINE_BIT_2OP | ( | ashr | ) |
| ESBMC_DEFINE_BIT_2OP | ( | bitand | ) |
| ESBMC_DEFINE_BIT_2OP | ( | bitor | ) |
| ESBMC_DEFINE_BIT_2OP | ( | bitxor | ) |
| ESBMC_DEFINE_BIT_2OP | ( | lshr | ) |
| ESBMC_DEFINE_BIT_2OP | ( | shl | ) |
| ESBMC_DEFINE_CODE_DECL | ( | code_dead | ) |
| ESBMC_DEFINE_CODE_EXPRESSION_1OP | ( | code_cpp_del_array | ) |
| ESBMC_DEFINE_CODE_EXPRESSION_1OP | ( | code_cpp_delete | ) |
| ESBMC_DEFINE_CODE_EXPRESSION_1OP | ( | code_expression | ) |
| ESBMC_DEFINE_CODE_EXPRESSION_1OP | ( | code_free | ) |
| ESBMC_DEFINE_CODE_EXPRESSION_1OP | ( | code_return | ) |
| ESBMC_DEFINE_FP_PREDICATE_1OP | ( | isfinite | ) |
| ESBMC_DEFINE_FP_PREDICATE_1OP | ( | isinf | ) |
| ESBMC_DEFINE_FP_PREDICATE_1OP | ( | isnan | ) |
| ESBMC_DEFINE_FP_PREDICATE_1OP | ( | isnormal | ) |
| ESBMC_DEFINE_IEEE_ARITH_2OP | ( | ieee_add | ) |
| ESBMC_DEFINE_IEEE_ARITH_2OP | ( | ieee_div | ) |
| ESBMC_DEFINE_IEEE_ARITH_2OP | ( | ieee_mul | ) |
| ESBMC_DEFINE_IEEE_ARITH_2OP | ( | ieee_rem | ) |
IEEE 754 remainder (SMT-LIB fp.rem, C's remainder()): x - n*y with n = rne(x/y).
Exact for every input, so the rounding mode the macro carries is ignored; it exists only to share the 2-op plumbing.
| ESBMC_DEFINE_IEEE_ARITH_2OP | ( | ieee_sub | ) |
| ESBMC_DEFINE_LOGIC_2OP | ( | and | ) |
| ESBMC_DEFINE_LOGIC_2OP | ( | hasattr | ) |
| ESBMC_DEFINE_LOGIC_2OP | ( | implies | ) |
| ESBMC_DEFINE_LOGIC_2OP | ( | isinstance | ) |
| ESBMC_DEFINE_LOGIC_2OP | ( | isnone | ) |
| ESBMC_DEFINE_LOGIC_2OP | ( | or | ) |
| ESBMC_DEFINE_LOGIC_2OP | ( | xor | ) |
| ESBMC_DEFINE_OBJECT_PREDICATE_1OP | ( | deallocated_obj | ) |
| ESBMC_DEFINE_OBJECT_PREDICATE_1OP | ( | races_check | ) |
| ESBMC_DEFINE_OBJECT_PREDICATE_1OP | ( | valid_object | ) |
| ESBMC_DEFINE_OBJECT_SIZE_1OP | ( | capability_base | ) |
| ESBMC_DEFINE_OBJECT_SIZE_1OP | ( | capability_top | ) |
| ESBMC_DEFINE_OBJECT_SIZE_1OP | ( | dynamic_size | ) |
| ESBMC_DEFINE_OVERFLOW_INT32_1OP | ( | popcount | ) |
| ESBMC_DEFINE_OVERFLOW_INT32_1OP | ( | signbit | ) |
| ESBMC_DEFINE_POINTER_1OP | ( | pointer_capability | ) |
| ESBMC_DEFINE_POINTER_1OP | ( | pointer_object | ) |
| ESBMC_DEFINE_RELATION2T | ( | equality | ) |
| ESBMC_DEFINE_RELATION2T | ( | greaterthan | ) |
| ESBMC_DEFINE_RELATION2T | ( | greaterthanequal | ) |
| ESBMC_DEFINE_RELATION2T | ( | lessthan | ) |
| ESBMC_DEFINE_RELATION2T | ( | lessthanequal | ) |
| ESBMC_DEFINE_RELATION2T | ( | notequal | ) |
| ESBMC_DEFINE_TYPE_ONLY | ( | invalid | ) |
| ESBMC_DEFINE_TYPE_ONLY | ( | null_object | ) |
| ESBMC_DEFINE_TYPE_ONLY | ( | unknown | ) |
| irep_typedefs | ( | abs | ) |
| irep_typedefs | ( | add | ) |
| irep_typedefs | ( | address_of | ) |
| irep_typedefs | ( | and | ) |
| irep_typedefs | ( | ashr | ) |
| irep_typedefs | ( | bitand | ) |
| irep_typedefs | ( | bitcast | ) |
| irep_typedefs | ( | bitnot | ) |
| irep_typedefs | ( | bitor | ) |
| irep_typedefs | ( | bitxor | ) |
| irep_typedefs | ( | bswap | ) |
| irep_typedefs | ( | byte_extract | ) |
| irep_typedefs | ( | byte_update | ) |
| irep_typedefs | ( | capability_base | ) |
| irep_typedefs | ( | capability_top | ) |
| irep_typedefs | ( | cmp_three_way | ) |
| irep_typedefs | ( | code_asm | ) |
| irep_typedefs | ( | code_assert | ) |
| irep_typedefs | ( | code_assign | ) |
| irep_typedefs | ( | code_assume | ) |
| irep_typedefs | ( | code_block | ) |
| irep_typedefs | ( | code_break | ) |
| irep_typedefs | ( | code_comma | ) |
| irep_typedefs | ( | code_continue | ) |
| irep_typedefs | ( | code_cpp_catch | ) |
| irep_typedefs | ( | code_cpp_del_array | ) |
| irep_typedefs | ( | code_cpp_delete | ) |
| irep_typedefs | ( | code_cpp_throw | ) |
| irep_typedefs | ( | code_dead | ) |
| irep_typedefs | ( | code_decl | ) |
| irep_typedefs | ( | code_dowhile | ) |
| irep_typedefs | ( | code_expression | ) |
| irep_typedefs | ( | code_for | ) |
| irep_typedefs | ( | code_free | ) |
| irep_typedefs | ( | code_function_call | ) |
| irep_typedefs | ( | code_goto | ) |
| irep_typedefs | ( | code_ifthenelse | ) |
| irep_typedefs | ( | code_label | ) |
| irep_typedefs | ( | code_printf | ) |
| irep_typedefs | ( | code_return | ) |
| irep_typedefs | ( | code_skip | ) |
| irep_typedefs | ( | code_switch | ) |
| irep_typedefs | ( | code_switch_case | ) |
| irep_typedefs | ( | code_while | ) |
| irep_typedefs | ( | concat | ) |
| irep_typedefs | ( | constant_array | ) |
| irep_typedefs | ( | constant_array_of | ) |
| irep_typedefs | ( | constant_bool | ) |
| irep_typedefs | ( | constant_fixedbv | ) |
| irep_typedefs | ( | constant_floatbv | ) |
| irep_typedefs | ( | constant_int | ) |
| irep_typedefs | ( | constant_string | ) |
| irep_typedefs | ( | constant_struct | ) |
| irep_typedefs | ( | constant_union | ) |
| irep_typedefs | ( | constant_vector | ) |
| irep_typedefs | ( | deallocated_obj | ) |
| irep_typedefs | ( | dereference | ) |
| irep_typedefs | ( | div | ) |
| irep_typedefs | ( | dynamic_object | ) |
| irep_typedefs | ( | dynamic_size | ) |
| irep_typedefs | ( | equality | ) |
| irep_typedefs | ( | exists | ) |
| irep_typedefs | ( | extract | ) |
| irep_typedefs | ( | forall | ) |
| irep_typedefs | ( | greaterthan | ) |
| irep_typedefs | ( | greaterthanequal | ) |
| irep_typedefs | ( | hasattr | ) |
| irep_typedefs | ( | ieee_add | ) |
| irep_typedefs | ( | ieee_div | ) |
| irep_typedefs | ( | ieee_fma | ) |
| irep_typedefs | ( | ieee_mul | ) |
| irep_typedefs | ( | ieee_rem | ) |
| irep_typedefs | ( | ieee_sqrt | ) |
| irep_typedefs | ( | ieee_sub | ) |
| irep_typedefs | ( | if | ) |
| irep_typedefs | ( | implies | ) |
| irep_typedefs | ( | index | ) |
| irep_typedefs | ( | invalid | ) |
| irep_typedefs | ( | invalid_pointer | ) |
| irep_typedefs | ( | isfinite | ) |
| irep_typedefs | ( | isinf | ) |
| irep_typedefs | ( | isinstance | ) |
| irep_typedefs | ( | isnan | ) |
| irep_typedefs | ( | isnone | ) |
| irep_typedefs | ( | isnormal | ) |
| irep_typedefs | ( | lessthan | ) |
| irep_typedefs | ( | lessthanequal | ) |
| irep_typedefs | ( | lshr | ) |
| irep_typedefs | ( | member | ) |
| irep_typedefs | ( | member_ref | ) |
| irep_typedefs | ( | modulus | ) |
| irep_typedefs | ( | mul | ) |
| irep_typedefs | ( | nearbyint | ) |
| irep_typedefs | ( | neg | ) |
| irep_typedefs | ( | new_object | ) |
| irep_typedefs | ( | not | ) |
| irep_typedefs | ( | notequal | ) |
| irep_typedefs | ( | null_object | ) |
| irep_typedefs | ( | object_descriptor | ) |
| irep_typedefs | ( | or | ) |
| irep_typedefs | ( | overflow | ) |
| irep_typedefs | ( | overflow_cast | ) |
| irep_typedefs | ( | overflow_neg | ) |
| irep_typedefs | ( | pointer_capability | ) |
| irep_typedefs | ( | pointer_object | ) |
| irep_typedefs | ( | pointer_offset | ) |
| irep_typedefs | ( | popcount | ) |
| irep_typedefs | ( | ptr_mem | ) |
| irep_typedefs | ( | races_check | ) |
| irep_typedefs | ( | same_object | ) |
| irep_typedefs | ( | shl | ) |
| irep_typedefs | ( | sideeffect | ) |
| irep_typedefs | ( | sideeffect_assign | ) |
| irep_typedefs | ( | signbit | ) |
| irep_typedefs | ( | sizeof | ) |
| irep_typedefs | ( | sub | ) |
| irep_typedefs | ( | symbol | ) |
| irep_typedefs | ( | typecast | ) |
| irep_typedefs | ( | uninterpreted_func | ) |
| irep_typedefs | ( | unknown | ) |
| irep_typedefs | ( | valid_object | ) |
| irep_typedefs | ( | with | ) |
| irep_typedefs | ( | xor | ) |
| printf_kindt printf_kind_from_name | ( | const irep_idt & | name | ) |
Maps the textual base_name of a printf-family symbol (e.g.
"printf", "snprintf") onto a printf_kindt. Aborts on an unknown name.
1.15.0