From 98930344e8c17d3f0db2b5fddcf774ac9db29629 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Fri, 29 Apr 2022 15:40:31 +0200 Subject: [PATCH] new tests with address state variables --- ..._address_inside_array_struct_trusted_1.sol | 23 ++++++++++++++++ ..._address_inside_array_struct_trusted_2.sol | 24 +++++++++++++++++ ...ate_var_address_inside_array_trusted_1.sol | 21 +++++++++++++++ ...ate_var_address_inside_array_trusted_2.sol | 20 ++++++++++++++ ...te_var_address_inside_struct_trusted_1.sol | 24 +++++++++++++++++ ...te_var_address_inside_struct_trusted_2.sol | 23 ++++++++++++++++ ...te_var_address_inside_struct_trusted_3.sol | 26 ++++++++++++++++++ ...te_var_address_inside_struct_trusted_4.sol | 27 +++++++++++++++++++ 8 files changed, 188 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol new file mode 100644 index 000000000..c4bab9c75 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol new file mode 100644 index 000000000..e8b9b5880 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_struct_trusted_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol new file mode 100644 index 000000000..541999b9f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_1.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol new file mode 100644 index 000000000..5abd44573 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_array_trusted_2.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol new file mode 100644 index 000000000..2ac70b33d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_1.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol new file mode 100644 index 000000000..e527c5bc0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_2.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol new file mode 100644 index 000000000..5563355e3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_3.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol new file mode 100644 index 000000000..63d026e52 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_state_var_address_inside_struct_trusted_4.sol @@ -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()