|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Classes | |
| class | _Lowering |
Functions | |
| _refuse (node, what, module_name) | |
| _binding_counts (module) | |
| _is_asyncio_run (call, counts) | |
| _evaluated_arguments (call, stmt) | |
| _is_generator (fn) | |
| lower_coroutines (module, module_name) | |
Run a module-level `async def` as a plain function where it is awaited. With no other task to switch to, `await f(x)` and `asyncio.run(f(x))` run the body of `f` to completion like `f(x)` would, and a call that is never awaited evaluates its arguments without running the body. A coroutine used any other way (stored, passed, scheduled) is refused, as is awaiting anything else.
|
protected |
|
protected |
`call`'s arguments as statements, evaluated as the unawaited call would.
|
protected |
|
protected |
|
protected |
| preprocessor.coroutine_lowering.lower_coroutines | ( | module, | |
| module_name ) |
Rewrite each module-level `async def` in `module` as a `def`.