SMTChecker docs test may issue a warning

hsienfu · Mar 10, 2020 · 1b17815 · 1b17815
1 parent 5fd5465
commit 1b17815
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/docs/security-considerations.rst b/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;

diff --git a/test/cmdlineTests.sh b/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
 )