|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
The coarse kinds of value (str, number, bool, None) a Python expression may produce, read from the module AST alone: the bindings of the names it reads, the arguments a parameter takes at every call site and its default, and what the functions and lambdas it calls return, following a function passed down a chain of parameters. More...
#include <value_kinds.h>
Public Member Functions | |
| value_kinds (const nlohmann::json &module) | |
| bool | diverges (const nlohmann::json &expr, const nlohmann::json &scope) |
| Whether expr, read in scope (a function definition or the module), may produce values of two different known kinds. | |
| const nlohmann::json & | scope_of (const std::string &function_name) const |
| The top-level function called function_name, or the module. | |
The coarse kinds of value (str, number, bool, None) a Python expression may produce, read from the module AST alone: the bindings of the names it reads, the arguments a parameter takes at every call site and its default, and what the functions and lambdas it calls return, following a function passed down a chain of parameters.
What it cannot read stays unknown, so two kinds are reported only when the program really mixes them.
|
explicit |
| bool value_kinds::diverges | ( | const nlohmann::json & | expr, |
| const nlohmann::json & | scope ) |
Whether expr, read in scope (a function definition or the module), may produce values of two different known kinds.
| const nlohmann::json & value_kinds::scope_of | ( | const std::string & | function_name | ) | const |
The top-level function called function_name, or the module.