solidity/test/libsolidity/smtCheckerTests/special/tx_data_immutable_fail.sol
Rodrigo Q. Saramago feba4de509
Add paris constraints to SMTChecker
Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org>
2023-01-31 11:03:04 +01:00

97 lines
3.7 KiB
Solidity

contract C {
bytes32 bhash;
address coin;
uint dif;
uint prevrandao;
uint glimit;
uint number;
uint tstamp;
bytes mdata;
address sender;
bytes4 sig;
uint value;
uint gprice;
address origin;
function f() public payable {
bhash = blockhash(12);
coin = block.coinbase;
dif = block.difficulty;
prevrandao = block.prevrandao;
glimit = block.gaslimit;
number = block.number;
tstamp = block.timestamp;
mdata = msg.data;
sender = msg.sender;
sig = msg.sig;
value = msg.value;
gprice = tx.gasprice;
origin = tx.origin;
fi();
assert(bhash == blockhash(122));
assert(coin != block.coinbase);
assert(dif != block.difficulty);
assert(prevrandao != block.prevrandao);
assert(glimit != block.gaslimit);
assert(number != block.number);
assert(tstamp != block.timestamp);
assert(mdata.length != msg.data.length);
assert(sender != msg.sender);
assert(sig != msg.sig);
assert(value != msg.value);
assert(gprice != tx.gasprice);
assert(origin != tx.origin);
}
function fi() internal view {
assert(bhash == blockhash(122));
assert(coin != block.coinbase);
assert(dif != block.difficulty);
assert(prevrandao != block.prevrandao);
assert(glimit != block.gaslimit);
assert(number != block.number);
assert(tstamp != block.timestamp);
assert(mdata.length != msg.data.length);
assert(sender != msg.sender);
assert(sig != msg.sig);
assert(value != msg.value);
assert(gprice != tx.gasprice);
assert(origin != tx.origin);
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 8417: (293-309): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (646-662): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 8417: (1129-1145): Since the VM version paris, "difficulty" was replaced by "prevrandao", which now returns a random number based on the beacon chain.
// Warning 6328: (563-594): CHC: Assertion violation happens here.
// Warning 6328: (598-628): CHC: Assertion violation happens here.
// Warning 6328: (632-663): CHC: Assertion violation happens here.
// Warning 6328: (667-705): CHC: Assertion violation happens here.
// Warning 6328: (709-741): CHC: Assertion violation happens here.
// Warning 6328: (745-775): CHC: Assertion violation happens here.
// Warning 6328: (779-812): CHC: Assertion violation happens here.
// Warning 6328: (816-855): CHC: Assertion violation happens here.
// Warning 6328: (859-887): CHC: Assertion violation happens here.
// Warning 6328: (891-913): CHC: Assertion violation happens here.
// Warning 6328: (917-943): CHC: Assertion violation happens here.
// Warning 6328: (947-976): CHC: Assertion violation happens here.
// Warning 6328: (980-1007): CHC: Assertion violation happens here.
// Warning 6328: (1046-1077): CHC: Assertion violation happens here.
// Warning 6328: (1081-1111): CHC: Assertion violation happens here.
// Warning 6328: (1115-1146): CHC: Assertion violation happens here.
// Warning 6328: (1150-1188): CHC: Assertion violation happens here.
// Warning 6328: (1192-1224): CHC: Assertion violation happens here.
// Warning 6328: (1228-1258): CHC: Assertion violation happens here.
// Warning 6328: (1262-1295): CHC: Assertion violation happens here.
// Warning 6328: (1299-1338): CHC: Assertion violation happens here.
// Warning 6328: (1342-1370): CHC: Assertion violation happens here.
// Warning 6328: (1374-1396): CHC: Assertion violation happens here.
// Warning 6328: (1400-1426): CHC: Assertion violation happens here.
// Warning 6328: (1430-1459): CHC: Assertion violation happens here.
// Warning 6328: (1463-1490): CHC: Assertion violation happens here.