SMTChecker docs test may issue a warning

This commit is contained in:
Leonardo Alt 2020-03-10 13:21:25 +01:00
parent 5fd5465f66
commit 1b17815808
2 changed files with 12 additions and 1 deletions

View File

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

View File

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