|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| bool | is_excluded_struct_tag_for_object_ref (const struct_typet &st) |
| bool | is_empty_user_class_object_type (const typet &type, const namespacet &ns) |
| int | get_list_compare_depth () |
| const nlohmann::json & | unwrap_optional_annotation (const nlohmann::json &ann) |
| static std::string | container_spelling (const nlohmann::json &slice) |
| The name a nested container element resolves by: its base, or the whole "Optional[T]", whose Optional<T> struct a bare "Optional" does not name (#8016). | |
| typet | get_elem_type_from_annotation (const nlohmann::json &node, const type_handler &type_handler_) |
| typet | get_elem_type_from_return_annotation (const nlohmann::json &function_node, const type_handler &type_handler_) |
| typet | infer_elem_type_from_call_return (const nlohmann::json &call_node, python_converter &converter) |
|
static |
The name a nested container element resolves by: its base, or the whole "Optional[T]", whose Optional<T> struct a bare "Optional" does not name (#8016).
| typet python_list_detail::get_elem_type_from_annotation | ( | const nlohmann::json & | node, |
| const type_handler & | type_handler_ ) |
| typet python_list_detail::get_elem_type_from_return_annotation | ( | const nlohmann::json & | function_node, |
| const type_handler & | type_handler_ ) |
| int python_list_detail::get_list_compare_depth | ( | ) |
| typet python_list_detail::infer_elem_type_from_call_return | ( | const nlohmann::json & | call_node, |
| python_converter & | converter ) |
| bool python_list_detail::is_empty_user_class_object_type | ( | const typet & | type, |
| const namespacet & | ns ) |
| bool python_list_detail::is_excluded_struct_tag_for_object_ref | ( | const struct_typet & | st | ) |
| const nlohmann::json & python_list_detail::unwrap_optional_annotation | ( | const nlohmann::json & | ann | ) |