ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
module_manager.cpp File Reference
#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>
Include dependency graph for module_manager.cpp:

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 &current_modules)
static std::vector< std::string > split (const std::string &str, char delimiter)

Function Documentation

◆ add_class_def()

void add_class_def ( module & md,
const nlohmann::json & node )
static

◆ add_function_def()

void add_function_def ( module & md,
const nlohmann::json & node,
const std::map< std::string, std::string > & aliases )
static

◆ annotated_return_type()

std::string annotated_return_type ( const nlohmann::json & returns)
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.

◆ get_module_recursive()

ModulePtr get_module_recursive ( const std::vector< std::string > & parts,
const ModulesList & current_modules )

◆ mentions_name()

bool mentions_name ( const nlohmann::json & node,
const std::string & name )
static

◆ module_aliases()

std::map< std::string, std::string > module_aliases ( const nlohmann::json & body)
static

Module-level X = T aliases, which an importer cannot resolve on its own.

◆ populate_module()

bool populate_module ( module & md,
const fs::path & json_path )
static

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.

◆ split()

std::vector< std::string > split ( const std::string & str,
char delimiter )
static

◆ string_annotation_type()

std::string string_annotation_type ( const nlohmann::json & returns)
static

A legacy forward reference, -> "int", and the -> None that shares its node type.