| 882 | } |
| 883 | |
| 884 | void SMTEncoder::visitGasLeft(FunctionCall const& _funCall) |
| 885 | { |
| 886 | std::string gasLeft = "gasleft"; |
| 887 | // We increase the variable index since gasleft changes |
| 888 | // inside a tx. |
| 889 | defineGlobalVariable(gasLeft, _funCall, true); |
| 890 | auto const& symbolicVar = m_context.globalSymbol(gasLeft); |
| 891 | unsigned index = symbolicVar->index(); |
| 892 | // We set the current value to unknown anyway to add type constraints. |
| 893 | m_context.setUnknownValue(*symbolicVar); |
| 894 | if (index > 0) |
| 895 | m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); |
| 896 | } |
| 897 | |
| 898 | void SMTEncoder::visitBlobHash(FunctionCall const& _funCall) |
| 899 | { |
nothing calls this directly
no test coverage detected