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

Functions

 _binds_only_its_name (stmt)
 _reads (stmt)
 _read_at_def_time (stmt)
 _ordered (run)
 _reordered (body)
 define_read_siblings_first (module)

Detailed Description

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`.

Function Documentation

◆ _binds_only_its_name()

preprocessor.sibling_defs._binds_only_its_name ( stmt)
protected

◆ _ordered()

preprocessor.sibling_defs._ordered ( run)
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.

◆ _read_at_def_time()

preprocessor.sibling_defs._read_at_def_time ( stmt)
protected

◆ _reads()

preprocessor.sibling_defs._reads ( stmt)
protected

◆ _reordered()

preprocessor.sibling_defs._reordered ( body)
protected

◆ define_read_siblings_first()

preprocessor.sibling_defs.define_read_siblings_first ( module)