|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| tuple[ast.AST, Preprocessor] | parse_file_canonicalised (str filename) |
| tuple[set[str], dict[str, str], set[str]|None] | _snapshot_exports (Preprocessor preprocessor) |
| tuple[set[str], dict[str, str]] | _compute_range_seed (ast.Module module_node, import_resolver) |
| None | _propagate_range_aliases_across_modules (dict parsed_trees, import_resolver) |
| tuple[set[str], dict[str, str], set[str]|None] | snapshot_exports (Preprocessor preprocessor) |
| tuple[set[str], dict[str, str]] | compute_range_seed (ast.Module module_node, import_resolver) |
| None | propagate_range_aliases_across_modules (dict parsed_trees, import_resolver) |
Cross-module range alias propagation helpers.
|
protected |
Build a (alias_seed, wrapper_seed) pair for *module_node*.
|
protected |
Re-apply alias / wrapper rewrites with cross-module seeds.
|
protected |
Snapshot a Preprocessor's range-alias / wrapper export tables.
| tuple[set[str], dict[str, str]] parser.range_alias_pipeline.compute_range_seed | ( | ast.Module | module_node, |
| import_resolver ) |
Public façade for range-seed projection.
| tuple[ast.AST, Preprocessor] parser.range_alias_pipeline.parse_file_canonicalised | ( | str | filename | ) |
Parse a file and run only the alias-canonicalisation pre-pass.
| None parser.range_alias_pipeline.propagate_range_aliases_across_modules | ( | dict | parsed_trees, |
| import_resolver ) |
Public façade for fixed-point alias propagation.
| tuple[set[str], dict[str, str], set[str] | None] parser.range_alias_pipeline.snapshot_exports | ( | Preprocessor | preprocessor | ) |
Public façade for exporter snapshotting.