- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
This is the complete list of members for andersent, including all inherited members.
| add_constraint(constraint_kindt kind, node_id lhs, node_id rhs) | andersent | |
| add_copy_edge(node_id from, node_id to) | andersent | protected |
| allocation(const type2tc &type, unsigned loc) | andersent | protected |
| allocators | andersent | protected |
| andersent() | andersent | |
| assign_node(const expr2tc &lhs, node_id src, unsigned loc) | andersent | protected |
| assign_top(const expr2tc &lhs, unsigned loc) | andersent | protected |
| bind_call(const irep_idt &callee_name, const goto_functiont &callee, const expr2tc &ret, const std::vector< expr2tc > &arguments, unsigned location_number) | andersent | protected |
| collect_constraints(const goto_functionst &goto_functions) | andersent | |
| constraint_kindt enum name | andersent | |
| constraints | andersent | protected |
| copy_edges | andersent | protected |
| ensure_node(node_id n) | andersent | protected |
| eval_address_of(const address_of2t &rhs, unsigned location_number) | andersent | protected |
| eval_branch(const if2t &rhs, unsigned location_number) | andersent | protected |
| eval_constant_aggregate(const expr2tc &rhs, unsigned location_number) | andersent | protected |
| eval_integer(const expr2tc &rhs, unsigned location_number) | andersent | protected |
| eval_pointer_arithmetic(const expr2tc &rhs, unsigned location_number) | andersent | protected |
| eval_realloc(node_id fresh, const expr2tc &old, unsigned location_number) | andersent | protected |
| eval_rhs(const expr2tc &rhs, unsigned location_number) | andersent | protected |
| eval_sideeffect(const sideeffect2t &rhs, unsigned location_number) | andersent | protected |
| eval_value(const expr2tc &rhs, unsigned location_number) | andersent | protected |
| everything_escapes | andersent | protected |
| expr_to_node | andersent | protected |
| find_node(const expr2tc &e) const | andersent | protected |
| fresh_node() | andersent | protected |
| get_node(const expr2tc &e) | andersent | |
| get_reference_set(locationt l, const expr2tc &expr, valuest &dest) override | andersent | virtual |
| get_values(locationt l, const expr2tc &expr, valuest &dest) override | andersent | virtual |
| handle_assign(const expr2tc &lhs, const expr2tc &rhs, unsigned location_number) | andersent | protected |
| handle_function_call(const code_function_call2t &call, const goto_functionst &goto_functions, unsigned location_number) | andersent | protected |
| handle_other(const expr2tc &code, unsigned location_number) | andersent | protected |
| has_location(locationt) const override | andersent | inlinevirtual |
| indirect_calls | andersent | protected |
| is_nondet_object(const expr2tc &object) | andersent | inlinestatic |
| join(node_id dst, node_id src) | andersent | protected |
| locationt typedef | value_setst | |
| may_point_to(node_id a, node_id b) const | andersent | |
| node_id typedef | andersent | |
| node_to_expr | andersent | protected |
| nondet_object_name | andersent | static |
| operator()(const goto_functionst &goto_functions) | andersent | |
| points_to(node_id n) const | andersent | |
| points_to_top(node_id n) | andersent | |
| pts | andersent | protected |
| reads_varargs | andersent | protected |
| resolve_indirect_calls(const goto_functionst &goto_functions) | andersent | protected |
| return_node(const irep_idt &fn) | andersent | protected |
| solve() | andersent | |
| solved | andersent | protected |
| symbol_to_node | andersent | protected |
| tmp_count | andersent | protected |
| to_object_descriptors(node_id n, valuest &dest) const | andersent | protected |
| TOP | andersent | static |
| top_source() | andersent | protected |
| unconstrained() | andersent | protected |
| value_setst()=default | value_setst | |
| valuest typedef | value_setst | |
| widen_call(const expr2tc &ret, const std::vector< expr2tc > &arguments, unsigned location_number) | andersent | protected |
| ~value_setst()=default | value_setst | virtual |
1.15.0