|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <python-frontend/module/module_manager.h>#include <python-frontend/module/module.h>#include <python-frontend/json_utils.h>#include <util/base/host_rounding_mode.h>#include <util/message/message.h>#include <nlohmann/json.hpp>#include <algorithm>#include <filesystem>#include <fstream>#include <map>Functions | |
| static std::string | string_annotation_type (const nlohmann::json &returns) |
| A legacy forward reference, -> "int", and the -> None that shares its node type. | |
| static std::string | annotated_return_type (const nlohmann::json &returns) |
| The return type named by a FunctionDef's annotation, or "" when it carries none. | |
| static std::map< std::string, std::string > | module_aliases (const nlohmann::json &body) |
| Module-level X = T aliases, which an importer cannot resolve on its own. | |
| static void | add_function_def (module &md, const nlohmann::json &node, const std::map< std::string, std::string > &aliases) |
| static void | add_class_def (module &md, const nlohmann::json &node) |
| static bool | mentions_name (const nlohmann::json &node, const std::string &name) |
| static bool | populate_module (module &md, const fs::path &json_path) |
Read json_path into md, reporting whether it could. | |
| ModulePtr | get_module_recursive (const std::vector< std::string > &parts, const ModulesList ¤t_modules) |
| static std::vector< std::string > | split (const std::string &str, char delimiter) |
|
static |
|
static |
|
static |
The return type named by a FunctionDef's annotation, or "" when it carries none.
"None" stands for an annotation this reader understands to be NoneType, so a caller cannot tell it apart from an unrecognised shape – which is the behaviour callers have always seen.
| ModulePtr get_module_recursive | ( | const std::vector< std::string > & | parts, |
| const ModulesList & | current_modules ) |
|
static |
|
static |
Module-level X = T aliases, which an importer cannot resolve on its own.
Read json_path into md, reporting whether it could.
Only functions, classes and overloads may be added here – see module::add_source for why. Diagnostics keep the create_module tag the messages have always carried.
|
static |
|
static |
A legacy forward reference, -> "int", and the -> None that shares its node type.