CBMC
|
Propagate. More...
Go to the source code of this file.
Functions | |
void | propagate (const std::vector< framet > &, const workt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &, const std::function< void(const symbol_exprt &, exprt, const workt::patht &)> &propagator) |
exprt | simplify_state_expr (exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &) |
exprt | simplify_state_expr_node (exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &) |
Propagate.
Definition in file propagate.h.
void propagate | ( | const std::vector< framet > & | frames, |
const workt & | work, | ||
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
bool | verbose, | ||
const namespacet & | ns, | ||
const std::function< void(const symbol_exprt &, exprt, const workt::patht &)> & | propagator | ||
) |
Definition at line 24 of file propagate.cpp.
exprt simplify_state_expr | ( | exprt | src, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns | ||
) |
Definition at line 1087 of file simplify_state_expr.cpp.
exprt simplify_state_expr_node | ( | exprt | src, |
const std::unordered_set< symbol_exprt, irep_hash > & | address_taken, | ||
const namespacet & | ns | ||
) |
Definition at line 961 of file simplify_state_expr.cpp.