solidity/test/libsolidity/smtCheckerTests/operators/ternary_operator_2.sol

contract C {

	function decrement(uint x) private pure returns (uint) {
		return x - 1; // No underflow, the method can be called only with positive value
	}

	function f(uint x) public pure returns (uint) {
		return x > 0 ? decrement(x) : 0;
	}
}
// ====
// SMTEngine: chc
// ----
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
[SMTChecker] Use path condition when creating CHC targets Without path condition, verification targets created inside ternary operator ignore the condition of the operator inside the branches. This led to false positives. Further updates: - Function calls should consider the conditions under which they are called, otherwise the analysis may report false positives. The fix proposed here is to add the current path condition to the edge that propagates error from a function call. - Increment error index after function call This is necessary for the analysis of the ternary operator to work correctly. No information should leak from a function call inside a ternary operator in the first branch to the second branch, including whether or not an error would have occured in the first branch. However, for the execution that continues after the function call, we still need to ensure that under the current path condition the error has not occurred in that function call. It would be better to isolate the analysis of the branches to separate clauses, but I do not see an easy way for that now. In this way, even though the function call in first branch is included in the clause of the second branch, no information leaks. - Additonal test for ternary operator This tests the behaviour of SMTChecker on ternary operator with function calls inside both branches. Specifically, it tests that SMTChecker successfully detects a violation of a verification target in the second branch when the same target is present also in the first branch, but there it cannot be triggered because of the operator's condition. 2023-02-11 20:56:13 +00:00			`contract C {`

			`function decrement(uint x) private pure returns (uint) {`
			`return x - 1; // No underflow, the method can be called only with positive value`
			`}`

			`function f(uint x) public pure returns (uint) {`
			`return x > 0 ? decrement(x) : 0;`
			`}`
			`}`
			`// ====`
			`// SMTEngine: chc`
			`// ----`
			`// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.`