|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| tuple[ast.AST, Preprocessor] | parse_file (str filename) |
| None | generate_ast_json (ast.AST tree, str python_filename, elements_to_import, str output_dir, str|None module_qualname=None) |
| None | emit_file_as_json (str filename, str output_dir, str|None module_qualname=None, elements_to_import=None) |
| None | emit_module_json (str module_qualname, str output_dir, elements_to_import=None) |
| str|None | _rejection_location (BaseException exc) |
| int|None | main () |
| int|None | _run_cli () |
Variables | |
| bootstrap = importlib.import_module(f"{__package__}.bootstrap") | |
| typecheck = importlib.import_module(f"{__package__}.typecheck") | |
| ensure_python3 = bootstrap.ensure_python3 | |
| ensure_python_frontend_on_path = bootstrap.ensure_python_frontend_on_path | |
| load_parser_module_deps = bootstrap.load_parser_module_deps | |
| run_mypy_strict = typecheck.run_mypy_strict | |
| _DEPS = load_parser_module_deps(__package__) | |
| add_type_annotation = _DEPS.constant_annotations.add_type_annotation | |
| annotate_constant_node = _DEPS.constant_annotations.annotate_constant_node | |
| tag_bignum_constants = _DEPS.constant_annotations.tag_bignum_constants | |
| tag_nonfinite_floats = _DEPS.constant_annotations.tag_nonfinite_floats | |
| _emit_file_as_json = _DEPS.json_emitter.emit_file_as_json | |
| _emit_module_json = _DEPS.json_emitter.emit_module_json | |
| _generate_ast_json = _DEPS.json_emitter.generate_ast_json | |
| EmitPipelineDeps = _DEPS.json_emitter.EmitPipelineDeps | |
| JsonEmitterDeps = _DEPS.json_emitter.JsonEmitterDeps | |
| cli_main = _DEPS.parser_cli.main | |
| CliDeps = _DEPS.parser_cli.CliDeps | |
| compute_range_seed = _DEPS.range_alias_pipeline.compute_range_seed | |
| propagate_range_aliases = _DEPS.range_alias_pipeline.propagate_range_aliases_across_modules | |
| snapshot_exports = _DEPS.range_alias_pipeline.snapshot_exports | |
| parse_file_canonicalised = _DEPS.range_alias_pipeline.parse_file_canonicalised | |
| import_resolver = _DEPS.import_resolver | |
| rewrite_re_match_attribute_calls = _DEPS.rewrite_re.rewrite_re_match_attribute_calls | |
| threading_lowering = _DEPS.threading_lowering | |
| int | _REJECTION_EXIT = 4 |
Thin façade/orchestrator for the Python frontend parser package.
|
protected |
`file:line:col` of the preprocessor frame that rejected the program.
|
protected |
| None parser.parser.emit_file_as_json | ( | str | filename, |
| str | output_dir, | ||
| str | None | module_qualname = None, | ||
| elements_to_import = None ) |
Wrapper around file JSON emission with parser-scoped dependencies.
| None parser.parser.emit_module_json | ( | str | module_qualname, |
| str | output_dir, | ||
| elements_to_import = None ) |
Wrapper around module JSON emission with parser-scoped dependencies.
| None parser.parser.generate_ast_json | ( | ast.AST | tree, |
| str | python_filename, | ||
| elements_to_import, | |||
| str | output_dir, | ||
| str | None | module_qualname = None ) |
Wrapper around json emitter with parser-scoped dependencies.
| int | None parser.parser.main | ( | ) |
Run parser CLI orchestration with assembled dependencies.
| tuple[ast.AST, Preprocessor] parser.parser.parse_file | ( | str | filename | ) |
Open, parse, and run Preprocessor on a Python source file.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
| parser.parser.add_type_annotation = _DEPS.constant_annotations.add_type_annotation |
| parser.parser.annotate_constant_node = _DEPS.constant_annotations.annotate_constant_node |
| parser.parser.bootstrap = importlib.import_module(f"{__package__}.bootstrap") |
| parser.parser.cli_main = _DEPS.parser_cli.main |
| parser.parser.CliDeps = _DEPS.parser_cli.CliDeps |
| parser.parser.compute_range_seed = _DEPS.range_alias_pipeline.compute_range_seed |
| parser.parser.EmitPipelineDeps = _DEPS.json_emitter.EmitPipelineDeps |
| parser.parser.ensure_python3 = bootstrap.ensure_python3 |
| parser.parser.ensure_python_frontend_on_path = bootstrap.ensure_python_frontend_on_path |
| parser.parser.import_resolver = _DEPS.import_resolver |
| parser.parser.JsonEmitterDeps = _DEPS.json_emitter.JsonEmitterDeps |
| parser.parser.load_parser_module_deps = bootstrap.load_parser_module_deps |
| parser.parser.parse_file_canonicalised = _DEPS.range_alias_pipeline.parse_file_canonicalised |
| parser.parser.propagate_range_aliases = _DEPS.range_alias_pipeline.propagate_range_aliases_across_modules |
| parser.parser.rewrite_re_match_attribute_calls = _DEPS.rewrite_re.rewrite_re_match_attribute_calls |
| parser.parser.run_mypy_strict = typecheck.run_mypy_strict |
| parser.parser.snapshot_exports = _DEPS.range_alias_pipeline.snapshot_exports |
| parser.parser.tag_bignum_constants = _DEPS.constant_annotations.tag_bignum_constants |
| parser.parser.tag_nonfinite_floats = _DEPS.constant_annotations.tag_nonfinite_floats |
| parser.parser.threading_lowering = _DEPS.threading_lowering |
| parser.parser.typecheck = importlib.import_module(f"{__package__}.typecheck") |