diff options
| author | chriseth <chris@ethereum.org> | 2018-12-17 21:09:52 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-17 21:09:52 +0800 |
| commit | 332f914e4ef45f92c89beb87a8bb02ba5e85592b (patch) | |
| tree | 02744cfff264720d3b58ea31703710b660ca121b /libsolidity/formal/SymbolicVariables.cpp | |
| parent | bf7d71d6b301a8eb4db0d06b7bf0ad1e6b67e679 (diff) | |
| parent | 9199718ec0aa1210094ceb9ca587fe49fba70518 (diff) | |
| download | dexon-solidity-332f914e4ef45f92c89beb87a8bb02ba5e85592b.tar dexon-solidity-332f914e4ef45f92c89beb87a8bb02ba5e85592b.tar.gz dexon-solidity-332f914e4ef45f92c89beb87a8bb02ba5e85592b.tar.bz2 dexon-solidity-332f914e4ef45f92c89beb87a8bb02ba5e85592b.tar.lz dexon-solidity-332f914e4ef45f92c89beb87a8bb02ba5e85592b.tar.xz dexon-solidity-332f914e4ef45f92c89beb87a8bb02ba5e85592b.tar.zst dexon-solidity-332f914e4ef45f92c89beb87a8bb02ba5e85592b.zip | |
Merge pull request #5388 from ethereum/smt_mapping
[SMTChecker] Support for mapping
Diffstat (limited to 'libsolidity/formal/SymbolicVariables.cpp')
| -rw-r--r-- | libsolidity/formal/SymbolicVariables.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 997635af..f7eeb3bd 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -127,3 +127,13 @@ smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _ar { return m_declaration(_arguments); } + +SymbolicMappingVariable::SymbolicMappingVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicVariable(move(_type), _uniqueName, _interface) +{ + solAssert(isMapping(m_type->category()), ""); +} |