cerc-io/solidity
11
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

new tests with address state variables

Browse Source
This commit is contained in:
Leo Alt 2022-04-29 15:40:31 +02:00
parent ff01c7275c
commit 98930344e8
8 changed files with 188 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol Normal file
View File

@ -0,0 +1,23 @@
contract D {
uint public x;
}
contract C {
struct S {
address d;
}
S[] ss;
constructor() {
ss.push(S(address(new D())));
assert(D(ss[0].d).x() == 0); // should hold
}
function f() public view {
assert(D(ss[0].d).x() == 0); // should hold, but fails because we havoc the state
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (210-237): CHC: Assertion violation happens here.

24
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol Normal file
View File

@ -0,0 +1,24 @@
contract D {
uint public x;
function setD(uint _x) public { x = _x; }
}
contract C {
struct S {
address d;
}
S[] ss;
constructor() {
ss.push(S(address(new D())));
assert(D(ss[0].d).x() == 0); // should hold
}
function f() public view {
assert(D(ss[0].d).x() == 0); // should fail
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (253-280): CHC: Assertion violation happens here.

21
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol Normal file
View File

@ -0,0 +1,21 @@
contract D {
uint public x;
function setD(uint _x) public { x = _x; }
}
contract C {
address[] ds;
constructor() {
ds.push(address(new D()));
assert(D(ds[0]).x() == 0); // should hold
}
function f() public view {
assert(D(ds[0]).x() == 0); // should fail
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (226-251): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x0]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x0]\nC.f()

20
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol Normal file
View File

@ -0,0 +1,20 @@
contract D {
uint public x;
}
contract C {
address[] ds;
constructor() {
ds.push(address(new D()));
assert(D(ds[0]).x() == 0); // should hold
}
function f() public view {
assert(D(ds[0]).x() == 0); // should hold, but fails because we havoc the state
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (183-208): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x0]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x0]\nC.f()

24
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol Normal file
View File

@ -0,0 +1,24 @@
contract D {
uint public x;
function setD(uint _x) public { x = _x; }
}
contract C {
struct S {
address d;
}
S s;
constructor() {
s.d = address(new D());
assert(D(s.d).x() == 0); // should hold
}
function f() public view {
assert(D(s.d).x() == 0); // should fail
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (240-263): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0x5039}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0x5039}\nC.f()

23
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol Normal file
View File

@ -0,0 +1,23 @@
contract D {
uint public x;
}
contract C {
struct S {
address d;
}
S s;
constructor() {
s.d = address(new D());
assert(D(s.d).x() == 0); // should hold
}
function f() public view {
assert(D(s.d).x() == 0); // should hold, but fails because we havoc the state
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (197-220): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0x5039}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0x5039}\nC.f()

26
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol Normal file
View File

@ -0,0 +1,26 @@
contract D {
uint public x;
}
contract C {
struct S {
address d;
}
struct T {
S s;
}
T t;
constructor() {
t.s.d = address(new D());
assert(D(t.s.d).x() == 0); // should hold
}
function f() public view {
assert(D(t.s.d).x() == 0); // should hold, but fails because we havoc the state
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (223-248): CHC: Assertion violation happens here.

27
test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol Normal file
View File

@ -0,0 +1,27 @@
contract D {
uint public x;
function setD(uint _x) public { x = _x; }
}
contract C {
struct S {
address d;
}
struct T {
S s;
}
T t;
constructor() {
t.s.d = address(new D());
assert(D(t.s.d).x() == 0); // should hold
}
function f() public view {
assert(D(t.s.d).x() == 0); // should fail
}
}
// ====
// SMTEngine: chc
// SMTExtCalls: trusted
// SMTTargets: assert
// ----
// Warning 6328: (266-291): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 0x5039}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 0x5039}}\nC.f()