|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| _binds_only_its_name (stmt) | |
| _reads (stmt) | |
| _read_at_def_time (stmt) | |
| _ordered (run) | |
| _reordered (body) | |
| define_read_siblings_first (module) | |
Define a function before the adjacent sibling defs that read it (#8960, #9034). Running an undecorated def whose defaults and annotations call nothing only binds its name, so the order of adjacent such defs cannot be observed. The converter resolves a sibling only once its def is converted, so `def g(): return h` followed by `def h()` refused `h`.
|
protected |
|
protected |
`run` with each def after the defs of `run` it reads, or `run` as it is when two defs share a name, read each other, or one reads at def time a name a def at or after it binds.
|
protected |
|
protected |
|
protected |
| preprocessor.sibling_defs.define_read_siblings_first | ( | module | ) |