diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 8e07d74d..e7481cca 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -57,6 +57,7 @@ private: virtual void endVisit(ExpressionStatement const& _node) override; virtual void endVisit(Assignment const& _node) override; virtual void endVisit(TupleExpression const& _node) override; + virtual void endVisit(UnaryOperation const& _node) override; virtual void endVisit(BinaryOperation const& _node) override; virtual void endVisit(FunctionCall const& _node) override; virtual void endVisit(Identifier const& _node) override; @@ -66,7 +67,12 @@ private: void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); - void assignment(Declaration const& _variable, Expression const& _value); + /// 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); // Visits the branch given by the statement, pushes and pops the SMT checker. // @param _condition if present, asserts that this condition is true within the branch. @@ -88,6 +94,9 @@ private: Expression const& _condition, std::string const& _description ); + /// Checks that the value is in the range given by the type. + void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, SourceLocation const& _location); + std::pair<smt::CheckResult, std::vector<std::string>> checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate); @@ -126,9 +135,12 @@ private: using VariableSequenceCounters = std::map<Declaration const*, int>; - /// Returns the expression corresponding to the AST node. Creates a new expression - /// if it does not exist yet. + /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. smt::Expression expr(Expression const& _e); + /// Creates the expression (value can be arbitrary) + void createExpr(Expression const& _e); + /// Creates the expression and sets its value. + void defineExpr(Expression const& _e, smt::Expression _value); /// Returns the function declaration corresponding to the given variable. /// The function takes one argument which is the "sequence number". smt::Expression var(Declaration const& _decl); |