solidity/test/cmdlineTests/model_checker_ext_calls_trusted_chc/err

Warning: Function state mutability can be restricted to pure
 --> model_checker_ext_calls_trusted_chc/input.sol:5:2:
  |
5 | 	function f() public view returns (uint) {
  | 	^ (Relevant source part starts here and spans across multiple lines).

Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
[SMTChecker] Add a new trusted mode which assumes that code that is available at compile time is trusted. 2021-10-12 09:12:18 +00:00			`Warning: Function state mutability can be restricted to pure`
			`--> model_checker_ext_calls_trusted_chc/input.sol:5:2:`
			`\|`
			`5 \| function f() public view returns (uint) {`
			`\| ^ (Relevant source part starts here and spans across multiple lines).`
Report safe properties in BMC and CHC 2023-02-09 16:07:13 +00:00
			`Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.`