diff options
author | chriseth <chris@ethereum.org> | 2018-03-01 19:24:11 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-01 19:24:11 +0800 |
commit | c123fa26f3a90090aa6d8f8ec028e362bfdb73a0 (patch) | |
tree | f7a34e452c816219c9a336f32ec6a90af8f53c4e /libsolidity/formal/SymbolicIntVariable.h | |
parent | cf6720eab5381a150c632eb484024a1a40a6a10f (diff) | |
parent | 8b1b4b78c043d54f493dc9e2330bf9df5cf93755 (diff) | |
download | dexon-solidity-c123fa26f3a90090aa6d8f8ec028e362bfdb73a0.tar.gz dexon-solidity-c123fa26f3a90090aa6d8f8ec028e362bfdb73a0.tar.zst dexon-solidity-c123fa26f3a90090aa6d8f8ec028e362bfdb73a0.zip |
Merge pull request #3406 from leonardoalt/smt_checker
SMTChecker: A little refactoring on SSA vars (preparation for Bool)
Diffstat (limited to 'libsolidity/formal/SymbolicIntVariable.h')
-rw-r--r-- | libsolidity/formal/SymbolicIntVariable.h | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h new file mode 100644 index 00000000..afa25f1b --- /dev/null +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -0,0 +1,50 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/formal/SymbolicVariable.h> + +#include <libsolidity/ast/Types.h> + +namespace dev +{ +namespace solidity +{ + +/** + * Specialization of SymbolicVariable for Integers + */ +class SymbolicIntVariable: public SymbolicVariable +{ +public: + SymbolicIntVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); + + /// Sets the var to 0. + void setZeroValue(int _seq); + /// Sets the variable to the full valid value range. + void setUnknownValue(int _seq); + + static smt::Expression minValue(IntegerType const& _t); + static smt::Expression maxValue(IntegerType const& _t); +}; + +} +} |