aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/analysis/SyntaxChecker.cpp2
-rw-r--r--libsolidity/formal/Why3Translator.cpp14
-rw-r--r--libsolidity/formal/Why3Translator.h1
3 files changed, 16 insertions, 1 deletions
diff --git a/libsolidity/analysis/SyntaxChecker.cpp b/libsolidity/analysis/SyntaxChecker.cpp
index a95b4879..dc8c1806 100644
--- a/libsolidity/analysis/SyntaxChecker.cpp
+++ b/libsolidity/analysis/SyntaxChecker.cpp
@@ -67,7 +67,7 @@ bool SyntaxChecker::visit(PragmaDirective const& _pragma)
{
solAssert(!_pragma.tokens().empty(), "");
solAssert(_pragma.tokens().size() == _pragma.literals().size(), "");
- if (_pragma.tokens()[0] != Token::Identifier && _pragma.literals()[0] != "solidity")
+ if (_pragma.tokens()[0] != Token::Identifier || _pragma.literals()[0] != "solidity")
syntaxError(_pragma.location(), "Unknown pragma \"" + _pragma.literals()[0] + "\"");
else
{
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index f3831b40..813fa3ab 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -757,6 +757,20 @@ bool Why3Translator::visit(Literal const& _literal)
return false;
}
+bool Why3Translator::visit(PragmaDirective const& _pragma)
+{
+ if (_pragma.tokens().empty())
+ error(_pragma, "Not supported");
+ else if (_pragma.literals().empty())
+ error(_pragma, "Not supported");
+ else if (_pragma.literals()[0] != "solidity")
+ error(_pragma, "Not supported");
+ else if (_pragma.tokens()[0] != Token::Identifier)
+ error(_pragma, "A literal 'solidity' is not an identifier. Strange");
+
+ return false;
+}
+
bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
{
return contains(m_currentContract.stateVariables, _var);
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 22bfff89..4fdac385 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -94,6 +94,7 @@ private:
virtual bool visit(IndexAccess const& _node) override;
virtual bool visit(Identifier const& _node) override;
virtual bool visit(Literal const& _node) override;
+ virtual bool visit(PragmaDirective const& _node) override;
virtual bool visitNode(ASTNode const& _node) override
{