aboutsummaryrefslogtreecommitdiffstats
path: root/test
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-10-23 00:19:11 +0800
committerLeonardo Alt <leo@ethereum.org>2018-10-23 00:19:11 +0800
commite2cf5f6ed94c571c7478b9a313f8e4fceee2aec3 (patch)
tree02beb0ee9b2db95e1e096ce7d3e7b41e94768f61 /test
parentb46b827c30584968c6815b456b8c0c775c35ae48 (diff)
downloaddexon-solidity-e2cf5f6ed94c571c7478b9a313f8e4fceee2aec3.tar.gz
dexon-solidity-e2cf5f6ed94c571c7478b9a313f8e4fceee2aec3.tar.zst
dexon-solidity-e2cf5f6ed94c571c7478b9a313f8e4fceee2aec3.zip
Add gasleft constraint and use full member access name
Diffstat (limited to 'test')
-rw-r--r--test/libsolidity/smtCheckerTests/special/difficulty.sol10
-rw-r--r--test/libsolidity/smtCheckerTests/special/gasleft.sol4
2 files changed, 14 insertions, 0 deletions
diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol
new file mode 100644
index 00000000..4469d4e5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+ function f(uint difficulty) public view {
+ assert(block.difficulty == difficulty);
+ }
+}
+// ----
+// Warning: (91-129): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol
index ec56d957..857230fe 100644
--- a/test/libsolidity/smtCheckerTests/special/gasleft.sol
+++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol
@@ -4,7 +4,11 @@ contract C
{
function f() public view {
assert(gasleft() > 0);
+ uint g = gasleft();
+ assert(g < gasleft());
+ assert(g >= gasleft());
}
}
// ----
// Warning: (76-97): Assertion violation happens here
+// Warning: (123-144): Assertion violation happens here