diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index d7f86cbc..34724848 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -47,10 +47,15 @@ class VariableUsage; class SMTChecker: private ASTConstVisitor { public: - SMTChecker(langutil::ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback); + SMTChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses); void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner); + /// This is used if the SMT solver is not directly linked into this binary. + /// @returns a list of inputs to the SMT solver that were not part of the argument to + /// the constructor. + std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); } + private: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined @@ -88,7 +93,7 @@ private: void inlineFunctionCall(FunctionCall const&); void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); - void defineUninterpretedFunction(std::string const& _name, std::vector<smt::SortPointer> const& _domain, smt::Sort const& _codomain); + void defineUninterpretedFunction(std::string const& _name, smt::SortPointer _sort); /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. @@ -157,8 +162,10 @@ private: /// Sets the value of the declaration to zero. void setZeroValue(VariableDeclaration const& _decl); + void setZeroValue(SymbolicVariable& _variable); /// Resets the variable to an unknown value (in its range). void setUnknownValue(VariableDeclaration const& decl); + void setUnknownValue(SymbolicVariable& _variable); /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. smt::Expression expr(Expression const& _e); |