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

Add SMTChecker tests with modules

Browse Source
This commit is contained in:
Leo Alt 2021-06-01 12:41:02 +02:00
parent 8eb28b10cb
commit 97a7c5429b
2 changed files with 6 additions and 6 deletions
test/libsolidity/smtCheckerTests/imports
import_as_module_1.solimport_as_module_2.sol

2
test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol
View File

@ -17,4 +17,4 @@ contract C {
// ====
// 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
// Warning 6328: (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

10
test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
View File

@ -18,9 +18,9 @@ function f(uint _x) pure {
// ====
// 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 8364: (118-119): Assertion checker does not yet implement type module "s1.sol"
// Warning 8364: (145-146): Assertion checker does not yet implement type module "s1.sol"
// Warning 6328: (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 f(10) -- internal call\n 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"
// Warning 8364: (118-119): Assertion checker does not yet implement type module "s1.sol"
// Warning 8364: (145-146): Assertion checker does not yet implement type module "s1.sol"