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

Add SMTCheckerTest isoltest option to ignore invariants

Browse Source
This commit is contained in:
Leo Alt 2021-10-06 11:51:55 +02:00
parent 3118fb3666
commit 37215ffcfd
3 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsolidity/formal/ModelCheckerSettings.h
View File

@ -95,6 +95,7 @@ struct ModelCheckerInvariants
static ModelCheckerInvariants Default() { return *fromString("default"); } static ModelCheckerInvariants Default() { return *fromString("default"); }
/// Adds all targets, including underflow and overflow. /// Adds all targets, including underflow and overflow.
static ModelCheckerInvariants All() { return *fromString("all"); } static ModelCheckerInvariants All() { return *fromString("all"); }
static ModelCheckerInvariants None() { return {{}}; }
static std::optional<ModelCheckerInvariants> fromString(std::string const& _invs); static std::optional<ModelCheckerInvariants> fromString(std::string const& _invs);

10
test/libsolidity/SMTCheckerTest.cpp
View File

@ -19,6 +19,8 @@
#include <test/libsolidity/SMTCheckerTest.h> #include <test/libsolidity/SMTCheckerTest.h>
#include <test/Common.h> #include <test/Common.h>
#include <range/v3/action/remove_if.hpp>
using namespace std; using namespace std;
using namespace solidity; using namespace solidity;
using namespace solidity::langutil; using namespace solidity::langutil;
@ -67,6 +69,14 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
else else
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice.")); BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice."));
auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "no");
if (ignoreInv == "no")
m_modelCheckerSettings.invariants = ModelCheckerInvariants::All();
else if (ignoreInv == "yes")
m_modelCheckerSettings.invariants = ModelCheckerInvariants::None();
else
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT invariant choice."));
auto const& ignoreOSSetting = m_reader.stringSetting("SMTIgnoreOS", "none"); auto const& ignoreOSSetting = m_reader.stringSetting("SMTIgnoreOS", "none");
for (string const& os: ignoreOSSetting | ranges::views::split(',') | ranges::to<vector<string>>()) for (string const& os: ignoreOSSetting | ranges::views::split(',') | ranges::to<vector<string>>())
{ {

2
test/libsolidity/SMTCheckerTest.h
View File

@ -49,6 +49,8 @@ protected:
Set in m_modelCheckerSettings. Set in m_modelCheckerSettings.
SMTIgnoreCex: `yes`, `no`, where the default is `no`. SMTIgnoreCex: `yes`, `no`, where the default is `no`.
Set in m_ignoreCex. Set in m_ignoreCex.
SMTIgnoreInv: `yes`, `no`, where the default is `no`.
Set in m_modelCheckerSettings.
SMTShowUnproved: `yes`, `no`, where the default is `yes`. SMTShowUnproved: `yes`, `no`, where the default is `yes`.
Set in m_modelCheckerSettings. Set in m_modelCheckerSettings.
SMTSolvers: `all`, `cvc4`, `z3`, `none`, where the default is `all`. SMTSolvers: `all`, `cvc4`, `z3`, `none`, where the default is `all`.