cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #1181 from ethereum/formal_ignore_pragma

Browse Source 
formal: ignore pragmas during Why3 code generation
This commit is contained in:
chriseth 2016-10-11 16:29:32 +02:00 committed by GitHub
commit 821fe6e916
2 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libsolidity/formal/Why3Translator.cpp
View File

@ -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);

1
libsolidity/formal/Why3Translator.h
View File

@ -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
{