-
Couldn't load subscription status.
- Fork 2.2k
Description
@mattsse @grandizzy @DaniPopes I think `require` should still be a branch. Can you check my reasoning?
There is a subtle difference between require and assert:
assertdeals with asserting invariants that should hold no matter what the input is. Hence why it shouldn't be possible to hit "the other branch" - that would indicate a bug in the code.requiredeals with pre/post conditions that may get violated due to erroneous/malicious inputs. Both sides of the branch need to be checked as both cases can occur. That's why we haveexpectRevertin tests.
There is a semantic difference and it's very well highlighted in the solidity docs:
Assert should only be used to test for internal errors, and to check invariants. Properly functioning code should never create a Panic, not even on invalid external input. If this happens, then there is a bug in your contract which you should fix. Language analysis tools can evaluate your contract to identify the conditions and function calls which will cause a Panic.
There is also a concrete/practical difference - the SMTChecker in solc relies on this distinction:
The SMTChecker module automatically tries to prove that the code satisfies the specification given by require and assert statements. That is, it considers require statements as assumptions and tries to prove that the conditions inside assert statements are always true. If an assertion failure is found, a counterexample may be given to the user showing how the assertion can be violated.
Does this make sense?
Originally posted by @KholdStare in #8413 (comment)