ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
parser.range_alias_pipeline Namespace Reference

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)

Detailed Description

Cross-module range alias propagation helpers.

Function Documentation

◆ _compute_range_seed()

tuple[set[str], dict[str, str]] parser.range_alias_pipeline._compute_range_seed ( ast.Module module_node,
import_resolver )
protected
Build a (alias_seed, wrapper_seed) pair for *module_node*.

◆ _propagate_range_aliases_across_modules()

None parser.range_alias_pipeline._propagate_range_aliases_across_modules ( dict parsed_trees,
import_resolver )
protected
Re-apply alias / wrapper rewrites with cross-module seeds.

◆ _snapshot_exports()

tuple[set[str], dict[str, str], set[str] | None] parser.range_alias_pipeline._snapshot_exports ( Preprocessor preprocessor)
protected
Snapshot a Preprocessor's range-alias / wrapper export tables.

◆ compute_range_seed()

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.

◆ parse_file_canonicalised()

tuple[ast.AST, Preprocessor] parser.range_alias_pipeline.parse_file_canonicalised ( str filename)
Parse a file and run only the alias-canonicalisation pre-pass.

◆ propagate_range_aliases_across_modules()

None parser.range_alias_pipeline.propagate_range_aliases_across_modules ( dict parsed_trees,
import_resolver )
Public façade for fixed-point alias propagation.

◆ snapshot_exports()

tuple[set[str], dict[str, str], set[str] | None] parser.range_alias_pipeline.snapshot_exports ( Preprocessor preprocessor)
Public façade for exporter snapshotting.