formal: ignore pragmas during Why3 code generation

Fixes #1177
This commit is contained in:
Yoichi Hirai 2016-10-07 15:32:47 +02:00
parent d3f410d8a8
commit 092e5829d8
2 changed files with 6 additions and 0 deletions

View File

@ -757,6 +757,11 @@ bool Why3Translator::visit(Literal const& _literal)
return false; return false;
} }
bool Why3Translator::visit(PragmaDirective const&)
{
return false;
}
bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const bool Why3Translator::isStateVariable(VariableDeclaration const* _var) const
{ {
return contains(m_currentContract.stateVariables, _var); return contains(m_currentContract.stateVariables, _var);

View File

@ -94,6 +94,7 @@ private:
virtual bool visit(IndexAccess const& _node) override; virtual bool visit(IndexAccess const& _node) override;
virtual bool visit(Identifier const& _node) override; virtual bool visit(Identifier const& _node) override;
virtual bool visit(Literal const& _node) override; virtual bool visit(Literal const& _node) override;
virtual bool visit(PragmaDirective const& _node) override;
virtual bool visitNode(ASTNode const& _node) override virtual bool visitNode(ASTNode const& _node) override
{ {