cerc-io/solidity
10
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

Use experimental feature pragma for SMT checker.

Browse Source
This commit is contained in:
chriseth 2017-08-11 18:54:56 +02:00
parent 75f09f2a84
commit c93f0434cd
2 changed files with 4 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libsolidity/ast/ExperimentalFeatures.h
View File

@ -29,6 +29,7 @@ namespace solidity
enum class ExperimentalFeature enum class ExperimentalFeature
{ {
SMTChecker,
ABIEncoderV2, // new ABI encoder that makes use of JULIA ABIEncoderV2, // new ABI encoder that makes use of JULIA
Test, Test,
TestOnlyAnalysis TestOnlyAnalysis
@ -36,11 +37,13 @@ enum class ExperimentalFeature
static const std::map<ExperimentalFeature, bool> ExperimentalFeatureOnlyAnalysis = static const std::map<ExperimentalFeature, bool> ExperimentalFeatureOnlyAnalysis =
{ {
{ ExperimentalFeature::SMTChecker, true },
{ ExperimentalFeature::TestOnlyAnalysis, true }, { ExperimentalFeature::TestOnlyAnalysis, true },
}; };
static const std::map<std::string, ExperimentalFeature> ExperimentalFeatureNames = static const std::map<std::string, ExperimentalFeature> ExperimentalFeatureNames =
{ {
{ "SMTChecker", ExperimentalFeature::SMTChecker },
{ "ABIEncoderV2", ExperimentalFeature::ABIEncoderV2 }, { "ABIEncoderV2", ExperimentalFeature::ABIEncoderV2 },
{ "__test", ExperimentalFeature::Test }, { "__test", ExperimentalFeature::Test },
{ "__testOnlyAnalysis", ExperimentalFeature::TestOnlyAnalysis }, { "__testOnlyAnalysis", ExperimentalFeature::TestOnlyAnalysis },

7
libsolidity/formal/SMTChecker.cpp
View File

@ -44,12 +44,7 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
void SMTChecker::analyze(SourceUnit const& _source) void SMTChecker::analyze(SourceUnit const& _source)
{ {
bool pragmaFound = false; if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
for (auto const& node: _source.nodes())
if (auto const* pragma = dynamic_cast<PragmaDirective const*>(node.get()))
if (pragma->literals()[0] == "checkAssertions")
pragmaFound = true;
if (pragmaFound)
{ {
m_interface->reset(); m_interface->reset();
m_currentSequenceCounter.clear(); m_currentSequenceCounter.clear();