| 1780 | } |
| 1781 | |
| 1782 | void SMTEncoder::defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex) |
| 1783 | { |
| 1784 | if (!m_context.knownGlobalSymbol(_name)) |
| 1785 | { |
| 1786 | bool abstract = m_context.createGlobalSymbol(_name, _expr); |
| 1787 | if (abstract) |
| 1788 | m_unsupportedErrors.warning( |
| 1789 | 1695_error, |
| 1790 | _expr.location(), |
| 1791 | "Assertion checker does not yet support this global variable." |
| 1792 | ); |
| 1793 | } |
| 1794 | else if (_increaseIndex) |
| 1795 | m_context.globalSymbol(_name)->increaseIndex(); |
| 1796 | // The default behavior is not to increase the index since |
| 1797 | // most of the global values stay the same throughout a tx. |
| 1798 | if (isSupportedType(*_expr.annotation().type)) |
| 1799 | defineExpr(_expr, m_context.globalSymbol(_name)->currentValue()); |
| 1800 | } |
| 1801 | |
| 1802 | bool SMTEncoder::shortcutRationalNumber(Expression const& _expr) |
| 1803 | { |
nothing calls this directly
no test coverage detected