diff options
| author | chriseth <chris@ethereum.org> | 2017-10-06 01:20:46 +0800 |
|---|---|---|
| committer | chriseth <chris@ethereum.org> | 2017-11-30 08:20:21 +0800 |
| commit | d160ec8595171e16dd404e9b859aa37aed2fe0a4 (patch) | |
| tree | d9cd357b2495143454bc5212aa55a8760cf41aa2 /libsolidity/formal/SMTChecker.h | |
| parent | 19e067465a058ca9f40238cb3a928a1113531c9d (diff) | |
| download | dexon-solidity-d160ec8595171e16dd404e9b859aa37aed2fe0a4.tar dexon-solidity-d160ec8595171e16dd404e9b859aa37aed2fe0a4.tar.gz dexon-solidity-d160ec8595171e16dd404e9b859aa37aed2fe0a4.tar.bz2 dexon-solidity-d160ec8595171e16dd404e9b859aa37aed2fe0a4.tar.lz dexon-solidity-d160ec8595171e16dd404e9b859aa37aed2fe0a4.tar.xz dexon-solidity-d160ec8595171e16dd404e9b859aa37aed2fe0a4.tar.zst dexon-solidity-d160ec8595171e16dd404e9b859aa37aed2fe0a4.zip | |
Fix signed division.
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index cc3aca81..e7481cca 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -67,6 +67,10 @@ private: void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); + /// Division expression in the given type. Requires special treatment because + /// of rounding for signed division. + smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); + void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location); void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); |