solidity/test/libsolidity/smtCheckerTests/out_of_bounds/array_3.sol
2021-04-08 21:03:39 +02:00

11 lines
307 B
Solidity

contract C {
uint[] a;
function r(uint i) public view returns (uint) {
return a[i]; // oob access
}
}
// ====
// SMTEngine: all
// ----
// Warning 6368: (82-86): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r(0)