|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Static Public Attributes | |
| set | specific_names [str] |
| TypeAlias | ParseFileCanonicalisedFn = Callable[[str], tuple[ast.AST, object]] |
| TypeAlias | RewriteRelativeImportFn = Callable[[ast.ImportFrom, str | None], None] |
| TypeAlias | SnapshotExportsFn = Callable[[object], tuple[set[str], dict[str, str], set[str] | None]] |
| TypeAlias | ParsedTreeState = dict[str, tuple[ast.AST, str, object]] |
| TypeAlias | PropagateRangeAliasesFn = Callable[[ParsedTreeState], None] |
| TypeAlias | GenerateAstJsonFn = Callable[[ast.AST, str, object, str, str | None], None] |
| dict | import_aliases = {} |
| dict | module_imports = {} |
| dict | module_exports = {} |
Static Protected Attributes | |
| set | _reported_cycles = set() |
| set | _reported_resolution_failures = set() |
| set | _reported_unmodelled = set() |
| dict | _unmodelled_modules = {} |
Per-module import aggregation used for deferred JSON emission.
|
staticprotected |
|
staticprotected |
|
staticprotected |
|
staticprotected |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |
|
static |