Merge pull request #8470 from ethereum/fix_smt_docs

SMTChecker docs test may issue a warning

docs/security-considerations.rst

@@ -547,6 +547,7 @@ not mean loss of proving power.
 
     pragma solidity >=0.5.0;
     pragma experimental SMTChecker;
+    // This may report a warning if no SMT solver available.
 
     contract Recover
     {
@@ -601,6 +602,7 @@ types.
     pragma solidity >=0.5.0;
     pragma experimental SMTChecker;
     // This will report a warning
+
     contract Aliasing
     {
         uint[] array;

test/cmdlineTests.sh

@@ -77,6 +77,11 @@ function compileFull()
         expect_output=1
         shift;
     fi
+    if [[ $1 = '-o' ]]
+    then
+        expect_output=2
+        shift;
+    fi
 
     local files="$*"
     local output
@@ -93,7 +98,7 @@ function compileFull()
     if [[ \
         "$exit_code" -ne "$expected_exit_code" || \
             ( $expect_output -eq 0 && -n "$errors" ) || \
-            ( $expect_output -ne 0 && -z "$errors" ) \
+            ( $expect_output -eq 1 && -z "$errors" ) \
     ]]
     then
         printError "Unexpected compilation result:"
@@ -350,6 +355,10 @@ SOLTMPDIR=$(mktemp -d)
         then
             opts="$opts -w"
         fi
+        if grep "This may report a warning" "$f" >/dev/null
+        then
+            opts="$opts -o"
+        fi
         compileFull $opts "$SOLTMPDIR/$f"
     done
 )

test/libsolidity/SMTCheckerJSONTest.cpp

@@ -17,14 +17,18 @@
 
 #include <test/libsolidity/SMTCheckerJSONTest.h>
 #include <test/Common.h>
+
+#include <libsolidity/formal/ModelChecker.h>
 #include <libsolidity/interface/StandardCompiler.h>
 #include <libsolutil/CommonIO.h>
 #include <libsolutil/JSON.h>
+
 #include <boost/algorithm/string.hpp>
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
 #include <boost/test/unit_test.hpp>
 #include <boost/throw_exception.hpp>
+
 #include <fstream>
 #include <memory>
 #include <stdexcept>
@@ -50,6 +54,9 @@ SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVer
 		!m_smtResponses.isObject()
 	)
 		BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
+
+	if (ModelChecker::availableSolvers().none())
+		m_shouldRun = false;
 }
 
 TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)