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

Merge pull request #11465 from ethereum/smt_add_modules_tests

Browse Source 
Add SMTChecker tests with modules
This commit is contained in:
Leonardo 2021-06-01 15:41:26 +02:00 committed by GitHub
commit 4df51020da
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 46 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol Normal file
View File

@ -0,0 +1,20 @@
==== Source: A ====
import "s1.sol" as M;
contract D is M.C {
function f(uint _y) public {
g(_y);
assert(x == _y); // should hold
assert(x > 100); // should fail
}
}
==== Source: s1.sol ====
contract C {
uint x;
function g(uint _x) public {
x = _x;
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (A:117-132): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: x = 0\nD.f(0)\n C.g(0) -- internal call

26
test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol Normal file
View File

@ -0,0 +1,26 @@
==== Source: A ====
import "s1.sol" as M;
function f(uint _x) pure {
assert(_x > 0);
}
contract D {
function g(uint _y) public pure {
M.f(200); // should hold
M.f(_y); // should fail
f(10); // should hold
f(_y); // should fail
}
}
==== Source: s1.sol ====
function f(uint _x) pure {
assert(_x > 100);
}
// ====
// SMTEngine: all
// ----
// Warning 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol"
// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol"
// Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call
// Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call
// Warning 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol"
// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol"